Inside 245-5D

Existential Pontification and Generalized Abstract Digressions

Equality, roughly speaking

In Software Foundations, equality is defined in this way: Even Coq's equality relation is not built in. It has (roughly) the following inductive definition. Inductive eq0 {X:Type} : X -> X -> Prop := refl_equal0 : forall x, eq0 x x. Why the roughly? Well, as it turns out, Coq defines equality a little differently […]

  • January 30, 2014