| 123456789101112131415161718192021222324252627282930313233343536 |
- -- This module is used to illustrate how to import a parameterised module.
- module examples.syntax.ModuleB
- (A : Set)
- ((==) : A -> A -> Prop)
- (refl : (x : A) -> x == x)
- where
- infix 5 /\
- module SubModule where
- postulate dummy : A
- data True : Prop where
- tt : True
- data False : Prop where
- data (/\) (P, Q : Prop) : Prop where
- andI : P -> Q -> P /\ Q
- data List : Set where
- nil : List
- cons : A -> List -> List
- eqList : List -> List -> Prop
- eqList nil nil = True
- eqList (cons x xs) nil = False
- eqList nil (cons y ys) = False
- eqList (cons x xs) (cons y ys) = x == y /\ eqList xs ys
- reflEqList : (xs : List) -> eqList xs xs
- reflEqList nil = tt
- reflEqList (cons x xs) = andI (refl x) (reflEqList xs)
|
