(>>) [Search_monad] | bind and return |
(>>|) [Search_monad] | non-deterministic choice |
A | |
aac_normalise [Aac_rewrite] | |
aac_reflexivity [Aac_rewrite] | |
aac_rewrite [Aac_rewrite] | |
add [Aac_rewrite] | |
add [Theory.Sigma] |
|
add_symbol [Theory.Trans] |
|
anomaly [Coq] | |
B | |
build [Coq.Rewrite] | build the constr to rewrite, with lambda abstractions |
C | |
choose [Search_monad] | |
count [Search_monad] | |
cps_resolve_one_typeclass [Coq] | |
D | |
debug [Helper.CONTROL] | |
debug [Helper.Debug] |
|
debug_exception [Helper.Debug] | |
decide_thm [Theory.Stubs] | The main lemma of our theory, that is
|
decomp_term [Coq] | |
E | |
empty [Theory.Sigma] |
|
empty_envs [Theory.Trans] | |
equal_aac [Matcher.Terms] | Test for equality of terms modulo AACU (relies on the following canonical representation of terms). |
eval [Theory.Stubs] | The evaluation fonction, used to convert a reified coq term to a raw coq term |
evar_binary [Coq] | |
evar_relation [Coq] | |
F | |
fail [Search_monad] | failure |
filter [Search_monad] | |
find_global [Coq] | |
fold [Search_monad] | folding through the collection |
from_relation [Coq.Equivalence] | |
G | |
get_efresh [Coq] | |
get_fresh [Coq] | |
get_hypinfo [Coq.Rewrite] |
|
I | |
infer [Coq.Equivalence] | |
instantiate [Matcher.Subst] | |
ir_of_envs [Theory.Trans] | |
ir_to_units [Theory.Trans] | |
is_empty [Search_monad] | |
L | |
lift [Theory.Stubs] | |
lift_normalise_thm [Theory.Stubs] | |
lift_proj_equivalence [Theory.Stubs] | |
lift_reflexivity [Theory.Stubs] | |
lift_transitivity_left [Theory.Stubs] | |
lift_transitivity_right [Theory.Stubs] | |
linear [Matcher] |
|
M | |
make [Coq.Equivalence] | |
make [Coq.Relation] | |
map_syms [Matcher.Terms] | |
match_as_equation [Coq] |
|
matcher [Matcher] |
|
mk_equivalence [Coq.Classes] | |
mk_letin [Coq] | |
mk_morphism [Coq.Classes] | |
mk_mset [Theory] | |
mk_pack [Theory.Sym] |
|
mk_reflexive [Coq.Classes] | |
mk_reifier [Theory.Trans] | |
mk_transitive [Coq.Classes] | |
N | |
nf_equal [Matcher.Terms] | |
nf_term_compare [Matcher.Terms] | |
none [Coq.Option] | |
null [Theory.Sym] |
|
O | |
of_int [Coq.Nat] | |
of_int [Coq.Pos] | |
of_list [Theory.Sigma] |
|
of_list [Coq.List] |
|
of_option [Coq.Option] | |
of_pair [Coq.Pair] | |
P | |
pair [Coq.Pair] | |
pr_aac_args [Aac_rewrite] | |
pr_constr [Helper.Debug] |
|
print [Print] | The main printing function. |
printing [Helper.CONTROL] | |
R | |
raw_constr_of_t [Theory.Trans] |
|
reif_constr_of_t [Theory.Trans] |
|
return [Search_monad] | |
rewrite [Coq.Rewrite] |
|
S | |
show_proof [Coq] | print the current proof term |
some [Coq.Option] | |
sort [Search_monad] | |
split [Coq.Equivalence] | |
split [Coq.Relation] | |
sprint [Matcher.Subst] | |
sprint [Search_monad] | |
sprint_nf_term [Matcher.Terms] | |
subterm [Matcher] |
|
T | |
t_of_constr [Theory.Trans] | |
t_of_term [Matcher.Terms] | |
tclDEBUG [Coq] | emit debug messages to see which tactics are failing |
tclPRINT [Coq] | print the current goal |
tclRETYPE [Coq] | |
tclTIME [Coq] | time the execution of a tactic |
term_of_t [Matcher.Terms] | we have the following property: |
time [Helper.CONTROL] | |
time [Helper.Debug] |
|
to_fun [Theory.Sigma] |
|
to_list [Matcher.Subst] | |
to_list [Search_monad] | |
to_relation [Coq.Equivalence] | |
typ [Theory.Sym] | |
typ [Coq.Nat] | |
typ [Coq.Pos] | |
typ [Coq.Option] | |
typ [Coq.Pair] | |
type_of_list [Coq.List] |
|
U | |
user_error [Coq] | |
W | |
warning [Coq] |