tur/equal

stdlib/equal.tur

type-equality witness (Equal GADT) for type-safe coercions.

Since: Phase G3

defn

equal-sym

(equal-sym [eq :Equal] :Equal)

defn

(equal-trans [eq1 :Equal eq2 :Equal] :Equal)

defn

(equal-cong [^f eq : (Equal a b)] :)

congruence: if a = b then (f a) = (f b) for any f : * -> *.

Parameters

a proof that a = b

Returns

A proof that (f a) = (f b).

Example

(equal-cong Refl)  ; => Refl

Since: Phase G4 (requires HKT)