ebacfee · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Equality result type

commitebacfee2fdfb49991230abd8c36892c0fb966aba authorBenjamin Saunders <besaunde@sfu.ca> dateThu 27 Dec 2012, 15:12 (14 years ago) parentdf10078

2 files changed+7−3

unifiedsplit

lib/Builtins.idr+4

@@ -76,6 +76,10 @@ boolElim False t e = e

7676

7777data so : Bool -> Type where oh : so True

7878

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+

7983syntax if [test] then [t] else [e] = boolElim test t e

8084syntax [test] "?" [t] ":" [e] = if test then t else e

8185

lib/Prelude/Bits.idr+3−3

@@ -200,11 +200,11 @@ bitsEq' {n=n} x y with (nextBits n)

200200 | Bits64 = prim__eqB64 x y

201201

202202public

203−bitsEq : (x : Bits n) -> (y : Bits n) -> Either (x = y -> _|_) (x = y)

203+bitsEq : (x : Bits n) -> (y : Bits n) -> Equality x y

204204bitsEq (MkBits x) (MkBits y) =

205205 case (bitsEq' x y) of

206− 0 => Left uneq

207− _ => Right eq

206+ 0 => Unequal uneq

207+ _ => Equal eq

208208 where

209209 postulate uneq : {x : Bits n} -> {y : Bits n} -> x = y -> _|_

210210 postulate eq : {x : Bits n} -> {y : Bits n} -> x = y