(>>) [Search_monad] |
bind and return
|
(>>|) [Search_monad] |
non-deterministic choice
|
A | |
add [Theory.Sigma] | add ty n x map adds the value x of type ty with key n in map
|
add_symbol [Theory.Trans] | add_symbol adds a given binary symbol to the environment of
known stuff.
|
anomaly [Coq] | |
B | |
build [Coq.Rewrite] |
build the constr to rewrite, in CPS style, with lambda abstractions
|
build_with_evar [Coq.Rewrite] |
build the constr to rewrite, in CPS style, with evars
|
C | |
choose [Search_monad] | |
count [Search_monad] | |
cps_evar_relation [Coq] | cps_mk_letin name v binds the constr v using a letin tactic
|
cps_from_relation [Coq.Equivalence] | |
cps_from_relation [Coq.Transitive] | |
cps_mk_letin [Coq] | |
cps_resolve_one_typeclass [Coq] | |
D | |
debug [Helper.CONTROL] | |
debug [Helper.Debug] | debug prints the string and end it with a newline
|
debug_exception [Helper.Debug] | |
decide_thm [Theory.Stubs] |
The main lemma of our theory, that is
compare (norm u) (norm v) = Eq -> eval u == eval v
|
decomp_term [Coq] | |
E | |
empty [Theory.Sigma] | empty ty create an empty map of type ty
|
empty_envs [Theory.Trans] | |
eq [Coq.Leibniz] | |
eq [Coq.Comparison] | |
eq_refl [Coq.Leibniz] | |
equal_aac [Matcher.Terms] |
Test for equality of terms modulo AACU (relies on the following
canonical representation of terms).
|
eval [Theory.Stubs] | |
evar_binary [Coq] | |
evar_relation [Coq] | |
evar_unit [Coq] | |
evm_compute [Evm_compute] | |
evm_compute_in [Evm_compute] | evm_compute eq blacklist h performs an evm_compute step in the hypothesis h
|
F | |
fail [Search_monad] |
failure
|
filter [Search_monad] | |
fold [Search_monad] |
folding through the collection
|
fresh_evar [Coq] | |
from_relation [Coq.Equivalence] | |
from_relation [Coq.Transitive] | |
G | |
get_hypinfo [Coq.Rewrite] | get_hypinfo H l2r ?check_type k analyse the hypothesis H, and
build the related hypinfo, in CPS style.
|
goal_update [Coq] | |
gt [Coq.Comparison] | |
I | |
infer [Coq.Equivalence] | |
infer [Coq.Transitive] | |
init_constant [Coq] | |
instantiate [Matcher.Subst] | |
ir_of_envs [Theory.Trans] | |
ir_to_units [Theory.Trans] | |
is_empty [Search_monad] | |
L | |
lapp [Coq] | |
lift [Theory.Stubs] | |
lift_normalise_thm [Theory.Stubs] | |
lift_proj_equivalence [Theory.Stubs] | |
lift_reflexivity [Theory.Stubs] |
The evaluation fonction, used to convert a reified coq term to a
raw coq term
|
lift_transitivity_left [Theory.Stubs] | |
lift_transitivity_right [Theory.Stubs] | |
linear [Matcher] | linear expands a multiset into a simple list
|
lt [Coq.Comparison] | |
M | |
make [Coq.Equivalence] | |
make [Coq.Transitive] | |
make [Coq.Relation] | |
match_as_equation [Coq] | match_as_equation ?context goal c try to decompose c as a
relation applied to two terms.
|
matcher [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 [Coq.Classes] | |
mk_morphism [Coq.Classes] | |
mk_mset [Theory] | |
mk_pack [Theory.Sym] | mk_pack rlt (ar,value,morph)
|
mk_reflexive [Coq.Classes] | |
mk_reifier [Theory.Trans] | |
mk_transitive [Coq.Classes] | |
N | |
nf_equal [Matcher.Terms] | |
nf_evar [Coq] | |
nf_term_compare [Matcher.Terms] | |
none [Coq.Option] | |
null [Theory.Sym] | null builds a dummy (identity) symbol, given an Coq.Relation.t
|
O | |
of_bool [Coq.Bool] | |
of_int [Coq.Nat] | |
of_int [Coq.Pos] | |
of_list [Theory.Sigma] | of_list ty null l translates an OCaml association list into a Coq one
|
of_list [Coq.List] | of_list ty l
|
of_option [Coq.Option] | |
of_pair [Coq.Pair] | |
P | |
pair [Coq.Pair] | |
pr_constr [Helper.Debug] | pr_constr print a Coq constructor, that can be labelled
by a string
|
print [Print] |
The main printing function.
|
printing [Helper.CONTROL] | |
R | |
raw_constr_of_t [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 [Theory.Trans] | reif_constr_of_t reifier t rebuilds the term t in the
reified form.
|
resolve_one_typeclass [Coq] | |
return [Search_monad] | |
rewrite [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 [Coq.Option] | |
sort [Search_monad] | |
split [Coq.Equivalence] | |
split [Coq.Relation] | |
sprint [Search_monad] | |
sprint [Matcher.Subst] | |
sprint_nf_term [Matcher.Terms] | |
subterm [Matcher] | subterm p t computes a set of solutions to the given
subterm-matching problem.
|
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
|
tclTIME [Coq] |
time the execution of a tactic
|
term_of_t [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 [Helper.CONTROL] | |
time [Helper.Debug] | time computes the time spent in a function, and then
print it using the given format
|
to_fun [Theory.Sigma] | to_fun ty null map converts a Coq association list into a Coq function (with default value null )
|
to_list [Search_monad] | |
to_list [Matcher.Subst] | |
to_relation [Coq.Equivalence] | |
to_relation [Coq.Transitive] | |
typ [Theory.Sym] | |
typ [Coq.Nat] | |
typ [Coq.Pos] | |
typ [Coq.Comparison] | |
typ [Coq.Bool] | |
typ [Coq.Pair] | |
type_of_list [Coq.List] | type_of_list ty
|
U | |
user_error [Coq] | |
W | |
warning [Coq] |