[][src]Module minitt::ast

Syntax: term, expression, context.

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

No dependency.

Structs

AnonymousValue

Just a wrapper for a value but does not do Eq comparison. This is an implementation detail and should not be noticed much when reading the source code.

Declaration

Decl in Mini-TT.

GenericCaseTree

Generic definition for three kinds of case trees

Enums

Closure

Clos in Mini-TT.

DeclarationType

Whether a type is recursive or not.

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.

Functions

branch_to_righted
nil_rc

Because we can't impl a Default for Rc.

reduce_to_value
up_dec_rc

Just for simplifying constructing an Rc.

up_var_rc

Just for simplifying constructing an Rc.

Type Definitions

Branch

Pattern matching branch.

CaseTree

SClos in Mini-TT.
Case tree.

GenericBranch
Neutral

Neut in Mini-TT, neutral value.

Telescope

Rho in Mini-TT, dependent context.

TelescopeRaw
TelescopeRc
Typed

Pattern with type explicitly specified