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](02_types/index), 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](