search

Andromedans / andromeda

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

printing types of terms in derivations #528

Closed anjapetkovic closed 4 years ago

anjapetkovic commented 4 years ago

When printing the derivations we can now see the type of the conclusion as well (relevant only if the conclusion is a term judgement). For example 

# rule A type;;
Rule A is postulated.
# rule a : A ;;
Rule a is postulated.
# derive -> a ;;
- :> derivation = derive → a : A