		Search-engine friendly clone of the ACL2 documentation.

Statements

Leo statements.

Here we formalize an abstract syntactic representation of all the Leo statements.

Asgop: Fixtype of Leo assignment operators.
Constdecl: Fixtype of constant declarations.
Console: Fixtype of Leo console calls.
Vardecl: Fixtype of variable declarations.
Vardecl-result: Fixtype of errors and Leo variable declarations.
Statement-result: Fixtype of errors and Leo statement.
Statement-list-result: Fixtype of errors and lists of Leo statements.
Constdecl-result: Fixtype of errors and Leo constant declarations.
Console-result: Fixtype of errors and Leo console function calls.
Branch-result: Fixtype of errors and Leo branches.
Branch-list-result: Fixtype of errors and lists of Leo branches
Asgop-result: Fixtype of errors and Leo assignment operators.
Asgop-to-binop: Map each Leo compound assignment operator to the corresponding binary operator.
Statement-fixtypes: Mutually recursive fixtypes of Leo statements.