Index of types

A
annot [Types]
B
bind_tyargs_order [Typed_ast]	A bind constant of a monad M has type `M 'a -> ('a -> M 'b) -> M 'b`.
C
c_env [Typed_ast]	`local_env` represents local_environments, i.e.
cdmap [Types]	`cdmap` is a type for maps of const_descr_ref.
checked_module [Typed_ast]
class_descr [Types]
class_val_spec [Typed_ast]
const_descr [Typed_ast]	The description of a top-level definition
const_descr_ref [Types]	A reference to a constant description.
const_descr_ref [Typed_ast]
const_target_rep [Typed_ast]
constr_family_descr [Types]
constraint_prefix [Typed_ast]
constraints [Typed_ast]
context [Precedence]
cr_special_fun [Typed_ast]
D
declare_def [Typed_ast]
def [Typed_ast]	A definition consists of a the real definition represented as a `def_aux`, followed by some white-space.
def_aux [Typed_ast]
def_macro [Def_trans]	`def_macro` is the type of definition macros.
defn_ctxt [Typecheck_ctxt]
do_line [Typed_ast]
dups [Util.Duplicate]
E
e_env [Typed_ast]
env [Typed_ast]
env_tag [Typed_ast]	`env_tag` is used by `const_descr` to describe the type of constant.
error [Reporting_basic]	In contrast to warnings, errors always kill the current run of Lem.
exp [Typed_ast]
exp_aux [Typed_ast]
exp_kind [Precedence]
exp_subst [Typed_ast]
F
f_env [Typed_ast]
fexp [Typed_ast]
fun_def_rec_flag [Typed_ast]	`fun_def_rec_flag` is used to encode, whether a `Fun_def` is recursive.
funcl_aux [Typed_ast]
I
i_env [Types]	an instance environment carries information about all defined instances
id [Types]	Represents a usage of an 'a (usually in constr_descr, field_descr, const_descr)
id_annot [Output]	kind annotation for latex'd identifiers
ident_option [Types]
imported_modules [Typed_ast]
indreln_indfn [Typed_ast]	Name and mode of a function to be generated from an inductive relation
indreln_name [Typed_ast]	Type annotation for the relation and information on what to generate from it.
indreln_rule [Typed_ast]
indreln_rule_aux [Typed_ast]	A rule of the form `Rule(clause_name_opt, sk1, sk2, bound_vars, sk3, left_hand_side_opt, sk4, rel_name, c, args)` encodes a clause `clause_name: forall bound_vars. (left_hand_side ==> rel_name args)`.
indreln_rule_quant_name [Typed_ast]
indreln_witness [Typed_ast]	Name of the witness type to be generated
instance [Types]	an instance of a type class
instance_ref [Types]	A reference to an instance.
instances [Process_file]
instschm [Typed_ast]	Instance Scheme, constraint prefix, sk, class-ident as printed, resolved class-path the id points to, instantiation type, sk
K
k [Finite_map.Dmap]
k [Finite_map.Fmap]
k [Finite_map.Dmap_map]
k [Finite_map.Fmap_map]
L
letbind [Typed_ast]
letbind_aux [Typed_ast]
level [Macro_expander]
lit [Typed_ast]
lit_aux [Typed_ast]
local_env [Typed_ast]
lskips [Typed_ast]	Whitespace, comments, and newlines
lskips_seplist [Typed_ast]
lskips_t [Name]	`lskips_t` is the type of names with immediately preceding skips, i.e.
M
m_env [Typed_ast]
macro [Trans]
macro_context [Macro_expander]
match_check_arg [Patterns]
match_props [Patterns]
mod_descr [Typed_ast]
mod_target_rep [Typed_ast]
N
n_uvar [Types]
name_kind [Typed_ast]
name_l [Typed_ast]
name_lskips_annot [Typed_ast]
name_sect [Typed_ast]
nexp [Types]
nexp_aux [Types]
non_ident_target [Target]	A datatype for Targets.
nvar [Typed_ast]
O
optsep [Seplist]
P
p_env [Typed_ast]	Maps a type name to the unique path representing that type and the first location this type is defined
parse_result [Pcombinators]
parser [Pcombinators]
pat [Typed_ast]
pat_annot [Typed_ast]
pat_aux [Typed_ast]
pat_context [Precedence]
pat_kind [Precedence]
pat_macro [Trans]
pat_pos [Macro_expander]
pat_position [Macro_expander]
Q
quant_binding [Typed_ast]
R
range [Types]
range [Typed_ast]
rel_info [Typed_ast]	rel_info represents information about functions and types genereated from this relation 0
rel_io [Typed_ast]	rel_io represents whether an argument of an inductive relation is considerred as an input or an output
rel_mode [Typed_ast]	rel_output_type specifies the type of the result
rel_output_type [Typed_ast]
S
src_nexp [Types]
src_nexp_aux [Types]
src_t [Types]
src_t_aux [Types]
T
t [Tyvar]
t [Types.TNvar]
t [Types]
t [Seplist]
t [Precedence]
t [Path]
t [Output]
t [Nvar]
t [Name]	t is the type of plain names, names are essentially strings
t [Ident]	t is the type of dot separated lists of names (with preceding lexical spacing), e.g.
t [Finite_map.Dmap]
t [Finite_map.Fmap]
t [Finite_map.Dmap_map]
t [Finite_map.Fmap_map]
t' [Output]
t_aux [Types]
t_uvar [Types]
target [Target]	`target` for the typechecked ast is either a real target as in the AST or the identity target
target_rep_rhs [Typed_ast]
targets_opt [Typed_ast]	targets_opt is represents a set of targets.
tc_def [Types]
texp [Typed_ast]	Type exepressions for defining types
tnvar [Types]
tnvar [Typed_ast]
typ_constraints [Types]
type_defs [Types]
type_descr [Types]	a type description *
type_target_rep [Types]	the target representation of a type
typschm [Typed_ast]
tyvar [Typed_ast]
U
used_entities [Typed_ast_syntax]	The type `used_entities` collects lists of used constant references, modules and types of some expression, definition, pattern ...
V
v_env [Typed_ast]
val_def [Typed_ast]
val_spec [Typed_ast]
var_avoid_f [Typed_ast]	`var_avoid_f` is a type of a tuple `(avoid_ty_vars, name_ok, do_rename)`.
W
warn_source [Reporting]	Warnings can be caused by definitions or expressions.
warning [Reporting]	Warnings are problems that Lem can deal with.