Alt-Ergo’s native language

This page documents Alt-Ergo’s native input language and its syntax.

In order to state a problem, the user may enrich the signature of the theory by adding new symbols and types, using keywords such as logic and type. Axioms can be declared through the axiom construct, and goals are set with goal. Additional constructs allow to define theories or to use if-then-else, let-bindings or pattern-matching. A full description of the syntax is available in the last chapter.