B | |
branch [TypeCore] | |
C | |
colors [Bash] |
A set of nice colors.
|
D | |
data_field_def [TypeCore] |
A field in a data type
|
data_type [TypeCore] | |
data_type_group [TypeCore] | |
datacon_exports [Exports] | |
db_index [TypeCore] |
In the surface syntax, variables are named.
|
decision [GMap.S] | |
definitions [ExpressionsCore] | |
derivation [Derivations] | |
E | |
either [Either] | |
element [GSet.S] | |
env [TransSurface] | |
env [TypeCore] |
This is the environment that we use throughout Mezzo.
|
env [KindCheck] | |
env [Interpreter] | |
error [TypeErrors] |
A
TypeErrors.raw_error is wrapped.
|
error [Lexer] |
The abstract type of lexer errors.
|
expression [ExpressionsCore] |
This is not very different from
SurfaceSyntax.expression .
|
F | |
fact [Fact] | |
field [ExpressionsCore] | |
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 [ExpressionsCore] | |
interface [ExpressionsCore] | |
J | |
judgement [Derivations] | |
K | |
key [GMap.S] | |
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] | |
node [LazyList] | |
P | |
parameter [Fact] | |
patexpr [ExpressionsCore] | |
pattern [ExpressionsCore] |
The type of patterns.
|
point [PersistentUnionFind] | |
property [Fact] | |
Q | |
quantifier [TypeCore] |
A quantifier is universal or existential.
|
R | |
raw_error [TypeErrors] |
Clients of this module will want to use the various errors offered.
|
rec_flag [ExpressionsCore] | |
resolved_datacon [TypeCore] | |
result [Derivations] |
Primitive operations return a result.
|
result [Permissions] |
The module internally can explore several solutions, but in order not to
propagate this complexity outside the
Permissions module, we chose to pick
either an arbitrary solution (along with the corresponding derivation), or an
arbitrary failed derivation.
|
rule [Derivations] | |
rule_instance [Derivations] | |
run_options [Driver] | |
S | |
sig_item [ExpressionsCore] | |
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 [LazyList] | |
t [GMap.S] | |
t [GSet.S] | |
t [InfiniteArray] | |
tag_update_info [ExpressionsCore] | |
tapp [ExpressionsCore] | |
token [Grammar] | |
toplevel_item [ExpressionsCore] | |
typ [TypeCore] |
The type of types.
|
type_binding [TypeCore] |
A type binding defines a type variable bound in a type.
|
type_def [TypeCore] | |
V | |
value_exports [Exports] | |
var [TypeCore] |
We adopt a locally nameless style; therefore, variables can be opened.
|
var [KindCheck] |
An environment maintains a mapping of external variable names to internal
objects, represented by the type
var .
|
variance [TypeCore] |
Our data constructors have the standard variance.
|