[−][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 |
Declaration |
|
GenericCase | Generic definition for three kinds of case trees |
Typed | $p:A$, Pattern with type explicitly specified. This is just a helper struct. |
Enums
Closure |
|
Expression |
|
GenericNeutral | Generic definition for two kinds of neutral terms. |
GenericTelescope | Generic definition for two kinds of telescopes. |
Pattern |
|
Value |
|
Functions
branch_to_righted | This function name is mysterious, but I failed to find a better name. It's for converting a
|
nil_rc | Because we can't |
up_dec_rc | Just for simplifying constructing an |
up_var_rc | Just for simplifying constructing an |
Type Definitions
Branch | $S ::= ()\ |\ (\textsf{c}\ M, S)$, Pattern matching branch. |
Case | One single case in case trees. |
CaseTree | $\lang S,\rho \rang$,
|
GenericBranch | $S(M) ::= ()\ |\ (\textsf{c}\ M, S)$ |
Level | |
Neutral | $k ::= k(v)$.
|
Telescope | $\rho ::= \rho(v)$
|
TelescopeRc |