search

Andromedans / andromeda

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

Implement general boundaries in premises. #526

Closed andrejbauer closed 4 years ago

andrejbauer commented 4 years ago

We implement premises of the form {x:A} ...{z:C} M :? c where c computes an abribtrary boundary. This is necessary in cases when the premise boundary needs to be computed, for example, using the equality checker with a local rule (that comes from a previous premise).

haselwarter commented 4 years ago

Should premises with specific boundaries be desugared into general boundaries?

andrejbauer commented 4 years ago

Good point. With @anjapetkovic we changed the code so that they are desugared in the parser already, and we also added general computed boundaries for rules.