view final_pre/src/AgdaParameterizedModule.agda @ 11:ef87093f92d4

add pdf
author e155702
date Sun, 17 Feb 2019 17:13:37 +0900
parents 0e8b9646d43f
children
line wrap: on
line source

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

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