@@ -75,6 +75,10 @@ f $ a = f a
7575cong : {f : t -> u} -> (a = b) -> f a = f b
7676cong refl = refl
7777
78+data Dec : Type -> Type where
79+ Yes : {A : Type} -> A -> Dec A
80+ No : {A : Type} -> (A -> _|_) -> Dec A
81+
7882data Bool = False | True
7983
8084boolElim : Bool -> |(t : a) -> |(f : a) -> a
@@ -83,10 +87,6 @@ boolElim False t e = e
8387
8488data so : Bool -> Type where oh : so True
8589
86−data Equality : {A : Type} -> (x : A) -> (y : A) -> Type where
87− Unequal : {A : Type} -> {x : A} -> {y : A} -> (x = y -> _|_) -> Equality x y
88− Equal : {A : Type} -> {x : A} -> {y : A} -> (x = y) -> Equality x y
89−
9090syntax if [test] then [t] else [e] = boolElim test t e
9191syntax [test] "?" [t] ":" [e] = if test then t else e
9292