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 [eq :Equal] :Equal)

defn

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

defn

(equal-cong [^f eq :(Equal a b)] :(Equal (f a) (f 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)