*Terms* are the logical *syntax.* All logical statements
are expressed as terms, and new term syntax is introduced with
the `declare` directive. All operations in the system are
defined on terms: all formal programs are interpreted as terms,
and all logical statements in the system are defined with terms.

Terms have a single uniform syntax, defined by the following syntax:

term::= operator{bterms}bterm::= term| vars.termoperator::= opname[params]opname::= literal | literal .opnameparam::= number :n| string:s| string:t| string:v|level:l|meta-parammeta-param::= var :n| var:s| var:t| var:vlevel::= number | literal | levelnumber |level'|level"|"level

A *simple* literal is any sequence of alphabetic and numeric
characters beginning with a letter. Additional literals are defined
as any sequence characters from the ASCII character set enclosed
in double quotes. A *string* is any sequence of characters
enclosed in double-quotes, and a *number* is any sequence
of digits. A *var* is a simple literal. The **bterms**
list uses the semicolon (`;`) as a separator
character, and the *vars* and **params** lists use a comma (`,`)
as a separator character. `:s` in parameters and meta-parameters
can be omitted.

The *operator* represents the *name* of a term, which
includes constant values defined by the parameters. The *opname*
is name, the *params* are the constant values, and the *bterms*
are the (possibly bound) subterms. If either of the *bterms*
and *params* list are empty in a term, the brackets may be
omitted.

Variables are a built-in term that are handled specially by the system.
There are two types of variables. *First-order* variables represent the
variable of the *object theory*. *Second-order*, or
*meta-level* variables represent terms with substitutions (second order
variables are used to define computational rewrites and inference rules). The
syntax of second-order variables represents substitutions with subterms.

The parser includes a simplifying syntax for variables: if
a simple literal is prefixed with an apostrophe (`'`),
the literal is interpreted as a variable. For example, the variable
*v* is represented with the syntax `'v`
Second order variables include their subterms in square brackets,
so `'v['v1; 'v2]` is the second-order variable `v` with two
arguments: `v1` and `v2`.

Term syntax is added to a module with the `declare`
directive. The *meaning* of the term is not defined at the
time of declaration; the meaning is defined with rewrites and
inference rules. Terms can represent constants, like the following
constants defined in `Itt_int` for numbers and `Itt_atom`
for strings.

declarenumber[i:n]declaretoken[s:t]

The declarations use *meta-syntax* for the parameters:
the natural number includes a *number* parameter, and the
token contains a *token* parameter. Once the meta-syntax
has been defined, terms can be included in ML programs as quotations:

letone = << number[1:n] >>lethello = << token["hello":t] >>

There is also a simplifying syntax for numbers: the parser
expands numbers to the `number` form when a term
is expected.

*Level-expressions* are included in the parameter syntax
to define type universes. For example, in the `Itt_equal`
module, type universes are declared as:

declareuniv[i:l]

and specific instances of type universes are the *base*
universe `univ[1:l]`, an *arbitrary* universe with
index *i* `univ[i:l]`, and relative universes like
`univ[i':l]` (which is the type universe containing `univ[i:l]`)
or `univ[(i | 3) : l]`, which is the smallest type universe
containing both `univ[3:l`] and `univ[i:l]`. Level
expressions can contain multiple indices: the universe `univ[(i
| j'):l]` is the minimum type universe containing both `univ[i:l]`
and `univ[j':l]`.

Expressions are also defined with the term syntax. For example,
the `Itt_int` module declares terms to represent arithmetic,
including the following:

declareadd{'x; 'y}declaresub{'x; 'y}

For these terms, the *opname* describes the arithmetic
operator, and the subterms represent numbers. The logical syntax
is *untyped*, the following terms are valid *syntax*,
although the second term has no meaning defined in the `Itt_theory`
module.

lettwo = << add{1; 1} >>leterror = << sub{3; token["hello":s]} >>

Expressions may also include binding. The `Itt_rfun`
module defines syntax for function abstraction and application.

declarelambda{x. 'b['x]}declareapply{'f; 'a}

*Binding* variables are simple literals (so they are not
quoted). The meta-syntax for `lambda` includes a second
order variable, indicating that the variable `'x` is *bound*
in the body `'b['x]` of the function. The following function
is an example of valid syntax in the `Itt_rfun` module:

letfour = << apply{lambda{x. add{'x; 'x}}; 2} >>.

This just syntax at this point: term evaluation has not yet been defined.

Types are also declared as terms. The syntax does not differentiate
between types and programs; the *meaning* of terms is defined
by computational rewriting and inference rules. The following
are some of the types defined in the `Itt_logic` module:

declare"true"declare"false"declare"and"{'A; 'B}declareall{'A; x. 'B['x]}

The `true`, `false` and `and` opnames have to be quoted here
so that the parser would not confuse them with OCaml keywords.

The uniform syntax is verbose: each term contains an operator,
and brackets for subterms. The verbosity can obscure the meaning
implied by term expressions. The page on display
forms discusses the pretty-printing mechanism for displaying
terms. The parser also provides a simplified syntax for commonly
occurring terms. The following tables list the operators for simplified syntax
in the priority order (starting from the lowest order to the highest order).
The right column gives term in the uniform
syntax. The simplified form is just an abbreviation; the term
must still be declared. For example, the use of the term `true
or false` requires that the term for

declare"true"declare"false"declare"or"{'A; 'B}lett = << "true"or"false" >>

t1=>t2implies{t1; t2}t1<=>t2iff{t1; t2}t1ort2or{t1; t2}t1andt2

t1&t2and{t1; t2}allx:t1. t2

exstx:t1. t2

foranyt1. t2

thereist1. t2

allx. t

exstx. t

allxInt1. t2

exstxInt1. t2all{t1; x. t2}

exists{t1; x. t2}

all{t1; self. t2}

exists{t1; self. t2}

sall{x. t}

sexists{x. t}

dall{t1; x. t2}

dexists{t1; x. t2}

_____

For

CZF

the-

ories

tType

t1=t2int<>

t1t2int

t1int=

t1t2

t1<>t2

t1subtypet2

t1subsett2

tint1subsett2

t1 ~ t2type{T}

equal{t; t1; t2}

nequal{t; t1; t2}

equal{t; t1; t1} or member{t1; t} (*)

equal{t1; t2}

nequal{t1; t2}

subtype{t1; t2)

subset{t1; t2)

member{t; t1; t2)

sqeq{t1; t2}t1<=t2

t1<t2

t1>=t2

t1>t2=@

t1t2

t1<>@t2<=@

t1t2

t1<@t2

t1>=@t2

t1>@t2le{t1; t2}

lt{t1; t2}

ge{t1; t2}

gt{t1; t2}

beq_int{t1; t2}

bneq_int{t1; t2}

le_bool{t1; t2}

lt_bool{t1; t2}

ge_bool{t1; t2}

lt_bool{t1; t2}

(*) The "*t1* **in ***t*" form is overloaded
— if only one of the two operators is declared, then the declared
operator is used, anf if both are declared, the `equal` form is used.

t1::t2cons{t1; t2}(t1, t2)pair{t1; t2}

t1->t2

x:t1->t2fun{t1; t2}

fun{t1; x.t2}t1*t2

x:t1*t2prod{t1; t2}prod{

t1; x. t2}t1+t2union{t1; t2}quotx, y: t1//t2

t1isectt2

x: t1isectt2

Isectx: t1.t2

t1uniont2

Unionx: t1.t2quot{t1; x, y. t2}

bisect{t1; t2}

bisect{t1; x. t2}

isect{t1; x. t2}

bunion{t1; t2}

tunion{t1; x. t2}

t1+@t2

t1-@t2add{t1; t2}

sub{t1; t2}- tminus{t}t1*@t2

t1/@t2

t1%@t2

t1 ^@ t2mul{t1; t2}

div{t1; t2}

rem{t1; t2}

power{t1; t2}

t1op[t]t2

t1 ^opt2

where op is *,+,/,-,^,

or >,<,=,<>,<=,>=t^"op"t1 t2^"op"

'selft1 t2

ift1thent2elset3

letx = t1int2

t2wherex = t1

opent1int2ifthenelse{t1; t2; t3}

let{t1;x.t2}

let{t1;x.t2}

let{t1;self.t2}

t1t2apply{t1; t2}t1^x

t1^x:=t2field["x":t]{t1}

rxrd["x":t]{t2;t1}

{x:t1|t2}set{t1; x.t2}{x:A; ... ;z:C}

{x:A; ... ;z:C; P}record[x:t]{A; self. . . .record[z:t]

{C}...}

{self:{x:A; ... ;z:C} | P}{x=a; ... ;z=c}rcrd[x:t]{a; . . . .

rcrd[z:t]{c}...}