Top-level commands

Theorem <NAME> : <FORMULA>.

Starts proof development with the given formula as the goal.

Theorem myTheorem : forall M N P, ...

Quit.

Exits from Adelfa.

Specification <QUOTED FILENAME>.

Reads in the specification indicated by the given filename.

Schema <ID> := <BLOCK SCHEMA>[; <BlOCK SCHEMA>].

Defines a context schema associated with <ID>.

A block schema has a, possibly empty, header of arity typed variables, followed by a series of, possibly empty, LF typed variables. A context schema can be comprised of any number of block schemas.

For example:

Schema C := {T:o}(x: tm, d: of x T);
            (x:tm, t:tp, d: of x t).

Set <OPTION> <VALUE>.

Sets the value of options during proof development. It may be used at the top level or inside theorem construction. The options are currently:

• search_depth The maximum number of times to perform type decomposition on assumption judgements during the search and assert tactics. Accepts any number as a <VALUE>. By default, this is set to 5.

Set search_depth 5.