@@ -75,6 +75,10 @@ f $ a = f a
75cong : {f : t -> u} -> (a = b) -> f a = f b
75cong : {f : t -> u} -> (a = b) -> f a = f b
76cong refl = refl
76cong refl = refl
78+data Dec : Type -> Type where
79+ Yes : {A : Type} -> A -> Dec A
80+ No : {A : Type} -> (A -> _|_) -> Dec A
78data Bool = False | True
82data Bool = False | True
80boolElim : Bool -> |(t : a) -> |(f : a) -> a
84boolElim : Bool -> |(t : a) -> |(f : a) -> a
@@ -83,10 +87,6 @@ boolElim False t e = e
84data so : Bool -> Type where oh : so True
88data so : Bool -> Type where oh : so True
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
90syntax if [test] then [t] else [e] = boolElim test t e
90syntax if [test] then [t] else [e] = boolElim test t e
91syntax [test] "?" [t] ":" [e] = if test then t else e
91syntax [test] "?" [t] ":" [e] = if test then t else e