tur/equal

stdlib/equal.tur

type-equality witness (the refined Equal type) for type-safe coercions.

(Equal a a) has one constructor Refl. Matching on Refl refines type variable a.

Since: Phase G3

defdata

Equal

(defdata Equal [a b] (Refl : (Equal a a)))

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)