some tests for equality checker

Andromedans / andromeda

A proof assistant for general type theories

http://www.andromeda-prover.org/

Other

297 stars 34 forks source link

Closed anjapetkovic closed 4 years ago

anjapetkovic commented 4 years ago

A few examples on how to use equality checker:

unit type with extensionality rule
simple products with computation rules for projections and extensionality rule. Eqchk can prove eta-rule.
natural numbers with normalization of induction principle.

jonsterling commented 4 years ago

Pretty cool :sunglasses: