| (>>) [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] |