git.iko.soy/Idris-dev
on master help sign in
Equality result type
ebacfeeBenjamin Saunders
lib/Builtins.idr+4
compare with master
unifiedsplit
@@ -76,6 +76,10 @@ boolElim False t e = e
76
76
77data so : Bool -> Type where oh : so True
77data so : Bool -> Type where oh : so True
78
78
79+data Equality : {A : Type} -> (x : A) -> (y : A) -> Type where
80+ Unequal : {A : Type} -> {x : A} -> {y : A} -> (x = y -> _|_) -> Equality x y
81+ Equal : {A : Type} -> {x : A} -> {y : A} -> (x = y) -> Equality x y
82+
79syntax if [test] then [t] else [e] = boolElim test t e
83syntax if [test] then [t] else [e] = boolElim test t e
80syntax [test] "?" [t] ":" [e] = if test then t else e
84syntax [test] "?" [t] ":" [e] = if test then t else e
81
85
lib/Prelude/Bits.idr+3−3
@@ -200,11 +200,11 @@ bitsEq' {n=n} x y with (nextBits n)
200 | Bits64 = prim__eqB64 x y
200 | Bits64 = prim__eqB64 x y
201
201
202public
202public
203−bitsEq : (x : Bits n) -> (y : Bits n) -> Either (x = y -> _|_) (x = y)
203+bitsEq : (x : Bits n) -> (y : Bits n) -> Equality x y
204bitsEq (MkBits x) (MkBits y) =
204bitsEq (MkBits x) (MkBits y) =
205 case (bitsEq' x y) of
205 case (bitsEq' x y) of
206− 0 => Left uneq
206+ 0 => Unequal uneq
207− _ => Right eq
207+ _ => Equal eq
208 where
208 where
209 postulate uneq : {x : Bits n} -> {y : Bits n} -> x = y -> _|_
209 postulate uneq : {x : Bits n} -> {y : Bits n} -> x = y -> _|_
210 postulate eq : {x : Bits n} -> {y : Bits n} -> x = y
210 postulate eq : {x : Bits n} -> {y : Bits n} -> x = y