Print type of a term judgement

Andromedans / andromeda

A proof assistant for general type theories

http://www.andromeda-prover.org/

Other

297 stars 34 forks source link

Closed andrejbauer closed 4 years ago

andrejbauer commented 5 years ago

When a term judgement is computed and printed out, it does not show the type of the term, e.g.:

# {x : A} x
- : judgement = ⊢ {x : A} x

This should probably be

# {x : A} x
- : judgement = ⊢ {x : A} x : A

anjapetkovic commented 5 years ago

[x] In runtime put printing environment to dynamic environment instead of lexical
[x] In nucleus implement function abstracted_judgement_with_boundary: judgement_abstraction -> (judgement * boundary) abstraction
[x] in nucleus implement printing of abstracted judgement with boundary
[x] runtime prints judgements with boundaries, which should only affect printing of term judgements.