[−][src]Module minitt::syntax

Syntax: term, expression, context.

Methods are defined in reduce/read_back modules but their documents are here.

No dependency.

Enums

Closure	`Clos` in Mini-TT.
Declaration	`Decl` in Mini-TT.
Expression	`Exp` in Mini-TT. Expression language for Mini-TT.
GenericNeutral	Generic definition for two kinds of neutral terms.
GenericTelescope	Generic definition for two kinds of telescopes. `Value` can be specialized with `Value<Name>` or `NormalExpression<Name>`.
Pattern	`Patt` in Mini-TT.
Value	`Val` in Mini-TT, value term.

Virtual trait, created to simplify trait bounds for identifiers.

up_dec_rc	Just for simplifying constructing an `Rc`.
up_var_rc	Just for simplifying constructing an `Rc`.

Branch	Pattern matching branch.
DeepClosure	`SClos` in Mini-TT. A closure that comes with a pattern, like the data type (sum) definition (all the constructors are pattern-like) or the function definition (it's built on top of a pattern tree)
GenericDeepClosure	Generic definition for two kinds of deep closures
Neutral	`Neut` in Mini-TT, neutral value.
Telescope	`Rho` in Mini-TT, dependent context.
TelescopeRaw