onthefly

on-the-fly declarations

Variables and constants can be declared on-the-fly (or inline). If an equation contains a qualified variable (see qualified term), i.e., <name>:<sort-name>, then from this point on within the current equation only <name> is declared as a variable of sort <sort-name>.

It is allowed to redeclare a previously defined variable name via an on-the-fly declaration, but as mentioned above, not via an explicit redeclaration.

Using a predeclared variable name within an equation first as is, that is as the predeclared variable, and later on in the same equation with an on-the-fly declaration is forbidden. That is, under the assumption that A has been declared beforehand, the following equation is not valid:

eq foo(A, A:S) = A .

On-the-fly declaration of constants are done the same way, where the <name> is a constant name as in ``a:Nat`. Using this construct is similar to defining an operator

op <name> : -> <sort>

or in the above example, op a : -> Nat ., besides that the on-the-fly declaration of constants, like to one of variables, is only valid in the current context (i.e., term or axiom). These constant definitions are quite common in proof scores.

Related: var