search

Andromedans / andromeda

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

Separate the "judgement or boundary" in `Syntax` #475

Closed andrejbauer closed 4 years ago

andrejbauer commented 5 years ago

Whenever we use judgement_or_boundary in type-checking, we should output syntax according to the result of type checking. For instance, if Desugared.AbstractAtom abstract over a judgement abstraction then we should output Syntax.AbstractAtomJudgement and if it is a boundary abstraction then we should output Syntax.AbstractAtomBoundary.

andrejbauer commented 4 years ago

This is going to become obsolete as soon as abstract c1 c2 accepts more general c2, so I am closing this.