Andromedans / andromeda

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

fixed normalizing types before extensionality phase #541

Closed anjapetkovic closed 4 years ago

anjapetkovic commented 4 years ago

We forgot to normalize types of equality boundaries before entering type-directed phase. This is fixed, but some issues arised with stacking converts, whish were avoided by calling the function that joins them together (without re-checking that types match).

Since types had to match while making the converts, this should not be a problem.