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