view Paper/src/AgdaParameterizedModule.agda.replaced @ 5:339fb67b4375

INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents c59202657321
children
line wrap: on
line source

module Sort (A : Set) (_<_ : A !$\rightarrow$! A !$\rightarrow$! Bool) where
sort : List A !$\rightarrow$! List A
sort = -- 実装は省略 ...

-- Parameterized Module により N.sort や B.sort が可能
open import Sort Nat  Nat._<_  as N
open import Sort Bool Bool._<_ as B