C | |
| colors [Bash] |
A set of nice colors.
|
D | |
| data_field_def [TypeCore] |
A field in a data type
|
| data_type_def [TypeCore] | |
| data_type_def_branch [TypeCore] | |
| data_type_group [TypeCore] | |
| db_index [TypeCore] |
In the surface syntax, variables are named.
|
| decision [GMap.S] | |
| declaration [Expressions] | |
| declaration_group [Expressions] | |
| derivation [Derivations] | |
E | |
| element [GSet.S] | |
| env [TypeCore] |
This is the environment that we use throughout Mezzo.
|
| env [Interpreter] | |
| equations [Fix.Make] | |
| error [TypeErrors] |
A
TypeErrors.raw_error is wrapped.
|
| error [Lexer] |
The abstract type of lexer errors.
|
| expression [Expressions] |
This is not very different from
SurfaceSyntax.expression.
|
F | |
| fact [Fact] | |
| field [Expressions] | |
| flavor [TypeCore] |
A type binding can be either user-provided, through a universal
quantification for instance, or auto-generated, by the desugaring pass for
instance.
|
H | |
| hypotheses [Fact] | |
| hypothesis [Fact] | |
I | |
| implementation [Expressions] | |
| interface [Expressions] | |
J | |
| judgement [Derivations] | |
K | |
| key [GMap.S] | |
| key [Fix.IMPERATIVE_MAPS] | |
| kind [Kind] | |
L | |
| location [TypeCore] |
Our locations are made up of ranges.
|
| location [PersistentRef] | |
M | |
| mode [Mode] | |
| mode [Mezzo] | |
| mode_constraint [TypeCore] | |
N | |
| name [TypeCore] |
The type of user-generated or auto-generated names.
|
| name [Identifier.Make] | |
P | |
| parameter [Fact] | |
| patexpr [Expressions] | |
| pattern [Expressions] |
The type of patterns.
|
| point [PersistentUnionFind] | |
| property [Fact] | |
| property [Fix.PROPERTY] | |
| property [Fix.Make] | |
R | |
| raw_error [TypeErrors] |
Clients of this module will want to use the various errors offered.
|
| rec_flag [Expressions] | |
| resolved_branch [TypeCore] | |
| resolved_datacon [TypeCore] |
Since data constructors are now properly scoped, they are resolved, that is,
they are either attached to a point, or a De Bruijn index, which will later
resolve to a point when we open the corresponding type definition.
|
| result [Derivations] |
Primitive operations return a result, that is, either
Some env along with
a good derivation, or None with a bad derivation.
|
| result [Permissions] | |
| rhs [Fix.Make] | |
| rule [Derivations] | |
| rule_instance [Derivations] | |
| run_options [Driver] | |
S | |
| sig_item [Expressions] | |
| state [Derivations] |
The type of chained premises.
|
| state [PersistentUnionFind] | |
| store [PersistentRef] | |
| substitution_kit [Expressions] |
To tame the combinatorial explosion, the binding functions in this module
return a substitution kit.
|
T | |
| t [Mark] | |
| t [Identifier.Make] | |
| t [Hashcons] | |
| t [GMap.S] | |
| t [GSet.S] | |
| t [InfiniteArray] | |
| t [Fix.IMPERATIVE_MAPS] | |
| tag_update_info [Expressions] | |
| tapp [Expressions] | |
| token [Grammar] | |
| toplevel_item [Expressions] | |
| typ [TypeCore] |
The type of types.
|
| type_binding [TypeCore] |
A type binding defines a type variable bound in a type.
|
| type_def [TypeCore] | |
U | |
| unresolved_branch [TypeCore] | |
V | |
| valuation [Fix.Make] | |
| var [TypeCore] |
We adopt a locally nameless style; therefore, variables can be opened.
|
| variable [Fix.Make] | |
| variance [TypeCore] |
Our data constructors have the standard variance.
|