Index of types

annot [Types]

bind_tyargs_order [Typed_ast]
A bind constant of a monad M has type M 'a -> ('a -> M 'b) -> M 'b.

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]

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_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_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_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 [Finite_map.Dmap]
k [Finite_map.Fmap]
k [Finite_map.Dmap_map]
k [Finite_map.Fmap_map]

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_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_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]

optsep [Seplist]

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]

quant_binding [Typed_ast]

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]

src_nexp [Types]
src_nexp_aux [Types]
src_t [Types]
src_t_aux [Types]

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]

used_entities [Typed_ast_syntax]
The type used_entities collects lists of used constant references, modules and types of some expression, definition, pattern ...

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).

warn_source [Reporting]
Warnings can be caused by definitions or expressions.
warning [Reporting]
Warnings are problems that Lem can deal with.