Andromedans / andromeda

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

Add AML support for creating meta variables. #529

Closed andrejbauer closed 4 years ago

andrejbauer commented 4 years ago

The syntax is meta x or meta _.

In checking-mode only meta x creates a fresh meta-variable whose name is derived from x and whose boundary is the checking boundary.

Future extensions can add additional support. Right now, once a meta-variable is created, it can never be removed.