Index of values


(>>) [AAC_search_monad]
bind and return
(>>|) [AAC_search_monad]
non-deterministic choice

A
add [AAC_theory.Sigma]
add ty n x map adds the value x of type ty with key n in map
add_symbol [AAC_theory.Trans]
add_symbol adds a given binary symbol to the environment of known stuff.
anomaly [AAC_coq]

B
build [AAC_coq.Rewrite]
build the constr to rewrite, in CPS style, with lambda abstractions
build_with_evar [AAC_coq.Rewrite]
build the constr to rewrite, in CPS style, with evars

C
choose [AAC_search_monad]
count [AAC_search_monad]
cps_evar_relation [AAC_coq]
cps_mk_letin name v binds the constr v using a letin tactic
cps_from_relation [AAC_coq.Equivalence]
cps_from_relation [AAC_coq.Transitive]
cps_mk_letin [AAC_coq]
cps_resolve_one_typeclass [AAC_coq]

D
debug [AAC_helper.CONTROL]
debug [AAC_helper.Debug]
debug prints the string and end it with a newline
debug_exception [AAC_helper.Debug]
decide_thm [AAC_theory.Stubs]
The main lemma of our theory, that is compare (norm u) (norm v) = Eq -> eval u == eval v
decomp_term [AAC_coq]

E
empty [AAC_theory.Sigma]
empty ty create an empty map of type ty
empty_envs [AAC_theory.Trans]
eq [AAC_coq.Comparison]
eq_refl [AAC_coq.Leibniz]
equal_aac [AAC_matcher.Terms]
Test for equality of terms modulo AACU (relies on the following canonical representation of terms).
eval [AAC_theory.Stubs]
evar_binary [AAC_coq]
evar_relation [AAC_coq]
evar_unit [AAC_coq]

F
fail [AAC_search_monad]
failure
filter [AAC_search_monad]
fold [AAC_search_monad]
folding through the collection
fresh_evar [AAC_coq]
from_relation [AAC_coq.Equivalence]
from_relation [AAC_coq.Transitive]

G
get_hypinfo [AAC_coq.Rewrite]
get_hypinfo H l2r ?check_type k analyse the hypothesis H, and build the related hypinfo, in CPS style.
goal_update [AAC_coq]
gt [AAC_coq.Comparison]

I
infer [AAC_coq.Equivalence]
infer [AAC_coq.Transitive]
init_constant [AAC_coq]
instantiate [AAC_matcher.Subst]
ir_of_envs [AAC_theory.Trans]
ir_to_units [AAC_theory.Trans]
is_empty [AAC_search_monad]

L
lapp [AAC_coq]
lift [AAC_theory.Stubs]
lift_normalise_thm [AAC_theory.Stubs]
lift_proj_equivalence [AAC_theory.Stubs]
lift_reflexivity [AAC_theory.Stubs]
The evaluation fonction, used to convert a reified coq term to a raw coq term
lift_transitivity_left [AAC_theory.Stubs]
lift_transitivity_right [AAC_theory.Stubs]
linear [AAC_matcher]
linear expands a multiset into a simple list
lt [AAC_coq.Comparison]

M
make [AAC_coq.Equivalence]
make [AAC_coq.Transitive]
make [AAC_coq.Relation]
match_as_equation [AAC_coq]
match_as_equation ?context goal c try to decompose c as a relation applied to two terms.
matcher [AAC_matcher]
matcher p t computes the set of solutions to the given top-level matching problem (p is the pattern, t is the term).
mk_equivalence [AAC_coq.Classes]
mk_morphism [AAC_coq.Classes]
mk_mset [AAC_theory]
mk_pack [AAC_theory.Sym]
mk_pack rlt (ar,value,morph)
mk_reflexive [AAC_coq.Classes]
mk_reifier [AAC_theory.Trans]
mk_transitive [AAC_coq.Classes]

N
nf_equal [AAC_matcher.Terms]
nf_evar [AAC_coq]
nf_term_compare [AAC_matcher.Terms]
none [AAC_coq.Option]
null [AAC_theory.Sym]
null builds a dummy (identity) symbol, given an AAC_coq.Relation.t

O
of_bool [AAC_coq.Bool]
of_int [AAC_coq.Nat]
of_int [AAC_coq.Pos]
of_list [AAC_theory.Sigma]
of_list ty null l translates an OCaml association list into a Coq one
of_list [AAC_coq.List]
of_list ty l
of_option [AAC_coq.Option]
of_pair [AAC_coq.Pair]

P
pair [AAC_coq.Pair]
pr_constr [AAC_helper.Debug]
pr_constr print a Coq constructor, that can be labelled by a string
print [AAC_print]
The main printing function.
printing [AAC_helper.CONTROL]

R
raw_constr_of_t [AAC_theory.Trans]
raw_constr_of_t rebuilds a term in the raw representation, and reconstruct the named products on top of it.
reif_constr_of_t [AAC_theory.Trans]
reif_constr_of_t reifier t rebuilds the term t in the reified form.
resolve_one_typeclass [AAC_coq]
return [AAC_search_monad]
rewrite [AAC_coq.Rewrite]
rewrite ?abort hypinfo subst builds the rewriting tactic associated with the given subst and hypinfo, and feeds it to the given continuation.

S
some [AAC_coq.Option]
sort [AAC_search_monad]
split [AAC_coq.Equivalence]
split [AAC_coq.Relation]
sprint [AAC_matcher.Subst]
sprint [AAC_search_monad]
sprint_nf_term [AAC_matcher.Terms]
subterm [AAC_matcher]
subterm p t computes a set of solutions to the given subterm-matching problem.

T
t_of_constr [AAC_theory.Trans]
t_of_term [AAC_matcher.Terms]
tclDEBUG [AAC_coq]
emit debug messages to see which tactics are failing
tclPRINT [AAC_coq]
print the current goal
tclTIME [AAC_coq]
time the execution of a tactic
term_of_t [AAC_matcher.Terms]
we have the following property: a and b are equal modulo AACU iif nf_equal (term_of_t a) (term_of_t b) = true
time [AAC_helper.CONTROL]
time [AAC_helper.Debug]
time computes the time spent in a function, and then print it using the given format
to_fun [AAC_theory.Sigma]
to_fun ty null map converts a Coq association list into a Coq function (with default value null)
to_list [AAC_matcher.Subst]
to_list [AAC_search_monad]
to_relation [AAC_coq.Equivalence]
to_relation [AAC_coq.Transitive]
typ [AAC_theory.Sym]
typ [AAC_coq.Nat]
typ [AAC_coq.Pos]
typ [AAC_coq.Comparison]
typ [AAC_coq.Bool]
typ [AAC_coq.Pair]
type_of_list [AAC_coq.List]
type_of_list ty

U
user_error [AAC_coq]

W
warning [AAC_coq]