sig
type t
type id
type location
val eq_t : Term_intf.Logic.t
val neq_t : Term_intf.Logic.t
val wildcard : Term_intf.Logic.t
val tType : Term_intf.Logic.t
val prop : Term_intf.Logic.t
val true_ : Term_intf.Logic.t
val false_ : Term_intf.Logic.t
val not_t : Term_intf.Logic.t
val or_t : Term_intf.Logic.t
val and_t : Term_intf.Logic.t
val xor_t : Term_intf.Logic.t
val nor_t : Term_intf.Logic.t
val nand_t : Term_intf.Logic.t
val equiv_t : Term_intf.Logic.t
val implied_t : Term_intf.Logic.t
val implies_t : Term_intf.Logic.t
val data_t : Term_intf.Logic.t
val var :
?loc:Term_intf.Logic.location -> Term_intf.Logic.id -> Term_intf.Logic.t
val const :
?loc:Term_intf.Logic.location -> Term_intf.Logic.id -> Term_intf.Logic.t
val atom : ?loc:Term_intf.Logic.location -> int -> Term_intf.Logic.t
val distinct :
?loc:Term_intf.Logic.location -> Term_intf.Logic.id -> Term_intf.Logic.t
val int : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
val rat : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
val real : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
val hexa : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
val binary : ?loc:Term_intf.Logic.location -> string -> Term_intf.Logic.t
val colon :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
val eq :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
val not_ :
?loc:Term_intf.Logic.location -> Term_intf.Logic.t -> Term_intf.Logic.t
val or_ :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t
val and_ :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t
val imply :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
val equiv :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
val apply :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t list -> Term_intf.Logic.t
val ite :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t ->
Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
val pi :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
val letin :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
val forall :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
val exists :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
val lambda :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
val choice :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
val description :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t -> Term_intf.Logic.t
val arrow :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
val product :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
val union :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
val subtype :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t -> Term_intf.Logic.t
val sequent :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t list -> Term_intf.Logic.t
val annot :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t -> Term_intf.Logic.t list -> Term_intf.Logic.t
val sexpr :
?loc:Term_intf.Logic.location ->
Term_intf.Logic.t list -> Term_intf.Logic.t
end