sig
val mk_mset : Term.constr -> (Term.constr * int) list -> Term.constr
module Sigma :
sig
val add :
Term.constr ->
Term.constr -> Term.constr -> Term.constr -> Term.constr
val empty : Term.constr -> Term.constr
val of_list :
Term.constr -> Term.constr -> (int * Term.constr) list -> Term.constr
val to_fun : Term.constr -> Term.constr -> Term.constr -> Term.constr
end
module Sym :
sig
type pack = {
ar : Term.constr;
value : Term.constr;
morph : Term.constr;
}
val typ : Term.constr lazy_t
val mk_pack : AAC_coq.Relation.t -> AAC_theory.Sym.pack -> Term.constr
val null : AAC_coq.Relation.t -> Term.constr
end
module Stubs :
sig
val lift : Term.constr Lazy.t
val lift_proj_equivalence : Term.constr Lazy.t
val lift_transitivity_left : Term.constr Lazy.t
val lift_transitivity_right : Term.constr Lazy.t
val lift_reflexivity : Term.constr Lazy.t
val eval : Term.constr lazy_t
val decide_thm : Term.constr lazy_t
val lift_normalise_thm : Term.constr lazy_t
end
module Trans :
sig
type envs
val empty_envs : unit -> AAC_theory.Trans.envs
val t_of_constr :
AAC_coq.goal_sigma ->
AAC_coq.Relation.t ->
AAC_theory.Trans.envs ->
Term.constr * Term.constr ->
AAC_matcher.Terms.t * AAC_matcher.Terms.t * AAC_coq.goal_sigma
val add_symbol :
AAC_coq.goal_sigma ->
AAC_coq.Relation.t ->
AAC_theory.Trans.envs -> Term.constr -> AAC_coq.goal_sigma
type ir
val ir_of_envs :
AAC_coq.goal_sigma ->
AAC_coq.Relation.t ->
AAC_theory.Trans.envs -> AAC_coq.goal_sigma * AAC_theory.Trans.ir
val ir_to_units : AAC_theory.Trans.ir -> AAC_matcher.ext_units
val raw_constr_of_t :
AAC_theory.Trans.ir ->
AAC_coq.Relation.t ->
Term.rel_context -> AAC_matcher.Terms.t -> Term.constr
type sigmas = {
env_sym : Term.constr;
env_bin : Term.constr;
env_units : Term.constr;
}
type reifier
val mk_reifier :
AAC_coq.Relation.t ->
Term.constr ->
AAC_theory.Trans.ir ->
(AAC_theory.Trans.sigmas * AAC_theory.Trans.reifier ->
Proof_type.tactic) ->
Proof_type.tactic
val reif_constr_of_t :
AAC_theory.Trans.reifier -> AAC_matcher.Terms.t -> Term.constr
end
end