Index of values


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