Std.Equal

View source →

Propositional equality combinators.

Eq(T, a, b) is the type of proofs that a and b are equal. The constructor refl(x) : Eq(T, x, x) witnesses reflexivity. The eliminator rewrite eq in expr substitutes equal terms in the type of expr while type-checking it.

All bindings here are erased at runtime: an Eq value lives only in the type checker. Every function returns the runtime atom :cure_refl.

Examples

use Std.Equal

refl(42)                                # : Eq(Int, 42, 42)
trans(refl(1), refl(1))                 # : Eq(Int, 1, 1)

Functions

  • # fn __group__() -> Atom

    Group tag consumed by Cure.Stdlib.Preload.

  • # fn cong(_f: (T) -> U, _eq: Atom) -> Atom

    Congruence: applying f preserves equality; from a == b derive f(a) == f(b).

  • # fn refl(_x: T) -> Atom

    Reflexivity: x equals itself. Produces the runtime witness :cure_refl with type Eq(T, x, x).

  • # fn sym(_eq: Atom) -> Atom

    Symmetry: if a == b, then b == a. Returns :cure_refl.

  • # fn trans(_p: Atom, _q: Atom) -> Atom

    Transitivity: if a == b and b == c, then a == c.