[−][src]Module minitt::syntax

Syntax: term, expression, context.

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

No dependency.

Structs

Decl in Mini-TT.

Closure	`Clos` in Mini-TT.
DeclarationType
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` or `NormalExpression`.
Pattern	`Patt` in Mini-TT.
Value	`Val` in Mini-TT, value term. Terms are either of canonical form or neutral form.

nil_rc	Because we can't `impl` a `Default` for `Rc`.
up_dec_rc	Just for simplifying constructing an `Rc`.
up_var_rc	Just for simplifying constructing an `Rc`.

Branch	Pattern matching branch.
CaseTree	`SClos` in Mini-TT. Case tree.
GenericCaseTree	Generic definition for two kinds of case trees
Neutral	`Neut` in Mini-TT, neutral value.
Telescope	`Rho` in Mini-TT, dependent context.
TelescopeRaw
TelescopeRc
Typed	Pattern with type explicitly specified