Up  Next

Module Context.Can


module Can: sig  end
val fnd : Th.t -> Context.t -> Term.t -> Term.t
Parameters:
th : Th.t
s : Context.t
a : Term.t
 
val findequiv : Th.t -> Context.t -> Term.t -> Term.t
Parameters:
th : Th.t
s : Context.t
a : Term.t


Canonization of terms 


val term : Context.t -> Term.t -> Term.t
Parameters:
s : Context.t
 
val can : Context.t -> Term.t -> Term.t
Parameters:
s : Context.t
a : Term.t
 
val pprod : Context.t -> Sym.pprod -> Term.t list -> Term.t
Parameters:
s : Context.t
op : Sym.pprod
al : Term.t list
 
val unsigned : Context.t -> Term.t -> Term.t
Parameters:
s : Context.t
x : Term.t
 
val arith : Context.t -> Sym.arith -> Term.t list -> Term.t
Parameters:
s : Context.t
op : Sym.arith
l : Term.t list
 
val eq : Context.t -> Term.t -> Term.t -> bool
Parameters:
s : Context.t
a : Term.t
b : Term.t


Canonization and normalization of atoms 


val atom : Context.t -> Atom.t -> Atom.t
Parameters:
s : Context.t
a : Atom.t
 
val equal : Context.t -> Term.t * Term.t -> Atom.t
Parameters:
s : Context.t
(a,b) : Term.t * Term.t
 
val diseq : Context.t -> Term.t * Term.t -> Atom.t
Parameters:
s : Context.t
(a,b) : Term.t * Term.t
 
val crossmultiply : Context.t -> Term.t * Term.t -> Term.t * Term.t
Parameters:
s : Context.t
(a,b) : Term.t * Term.t
 
val crossmultiply1 : Context.t -> Term.t * Term.t -> Term.t * Term.t
Parameters:
s : Context.t
(a,b) : Term.t * Term.t
 
val sign : Context.t -> Term.t * Sign.t -> Atom.t
Parameters:
s : Context.t
(a,i) : Term.t * Sign.t
 
val eq : Context.t -> Term.t -> Term.t -> bool
Parameters:
s : Context.t
a : Term.t
b : Term.t