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](01_declaration_of_symbols.md) and [types](02_types/index), using keywords such as logic and type. [Axioms](03_declaration_of_axioms.md) can be declared through the axiom construct, and [goals](04_setting_goals.md) are set with goal. Additional constructs allow to define [theories](05_theories.md) or to use [if-then-else, let-bindings or pattern-matching](06_control_flow.md). A full description of the syntax is available in [the last chapter](07_syntax_of_declarations_and_expressions.md).