Andromedans / andromeda

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

Have congruence rules handle atoms as well. #508

Closed andrejbauer closed 4 years ago

andrejbauer commented 4 years ago

The rationale is: it can handle constants, so perhaps it should also handle atoms. The user will be less surprised that congruence x x doesn't fail on atoms.