Andromedans / andromeda

A proof assistant for general type theories
http://www.andromeda-prover.org/
Other
297 stars 34 forks source link

Linear patterns #544

Closed anjapetkovic closed 1 month ago

anjapetkovic commented 2 years ago

In the equality checking algorithm we introduce linear patterns and computation rules and extensionality rules need to allow for equational premises.