tur/equal
stdlib/equal.tur
type-equality witness (Equal GADT) for type-safe coercions.
Since: Phase G3
defgadt
Equal
(defgadt Equal [a b] (Refl) (Equal))
defn
equal-sym
(equal-sym [eq : Equal] :)
defn
equal-trans
(equal-trans [eq1 : Equal eq2 : Equal] :)
defn
equal-cong
(equal-cong [^f eq : (Equal a b)] :)
congruence: if a = b then (f a) = (f b) for any f : * -> *.
Parameters
| eq | a proof that a = b |
Returns
A proof that (f a) = (f b).
Example
(equal-cong Refl) ; => Refl
Since: Phase G4 (requires HKT)