4 Cic.term * (* left side *)
5 Cic.term) * (* right side *)
6 Cic.metasenv * (* environment for metas *)
7 Cic.term list (* arguments *)
10 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
14 Performs the beta expansion of the term "where" w.r.t. "what",
15 i.e. returns the list of all the terms t s.t. "(t what) = where".
18 ?metas_ok:bool -> ?match_only:bool -> Cic.term -> Cic.term -> Cic.term ->
19 Cic.context -> Cic.metasenv -> CicUniv.universe_graph ->
20 (Cic.term * Cic.substitution * Cic.metasenv * CicUniv.universe_graph) list
24 scans the context to find all Declarations "left = right"; returns a
25 list of tuples (proof, (type, left, right), newmetas). Uses
26 PrimitiveTactics.new_metasenv_for_apply to replace bound variables with
30 ?eq_uri:UriManager.uri -> Cic.context -> ProofEngineTypes.proof ->
34 exception TermIsNotAnEquality;;
37 raises TermIsNotAnEquality if term is not an equation.
38 The first Cic.term is a proof of the equation
40 val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term ->
44 superposition_left env target source
45 returns a list of new clauses inferred with a left superposition step
46 the negative equation "target" and the positive equation "source"
48 val superposition_left: environment -> equality -> equality -> equality list
51 superposition_right newmeta env target source
52 returns a list of new clauses inferred with a right superposition step
53 the positive equations "target" and "source"
54 "newmeta" is the first free meta index, i.e. the first number above the
55 highest meta index: its updated value is also returned
57 val superposition_right:
58 int -> environment -> equality -> equality -> int * equality list
60 val demodulation: int -> environment -> equality -> equality -> int * equality
62 val meta_convertibility: Cic.term -> Cic.term -> bool
64 val meta_convertibility_eq: equality -> equality -> bool