-- 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)