Most objects that have a special meaning in logic are represented by a builtin. A builtin is a value of type t; it might correspond to different names in different input syntaxes.
Builtins cover numbers, connectives, and builtin types, among others.
val _t_bigger_false : bool reftype t = | Not| And| Or| Imply| Equiv| Xor| Eq| Neq| HasType| True| False| Arrow| Wildcard| Multiset| TType| Prop| Term| ForallConstconstant for simulating forall
*)| ExistsConstconstant for simulating exists
*)| ChoiceConst| Groundingused for inst-gen
*)| TyInt| TyRat| TyReal| Int of Logtk_arith.Z.t| Rat of Logtk_arith.Q.t| Real of string| Floor| Ceiling| Truncate| Round| Prec| Succ| Sum| Difference| Uminus| Product| Quotient| Quotient_e| Quotient_t| Quotient_f| Remainder_e| Remainder_t| Remainder_f| Is_int| Is_rat| To_int| To_rat| Less| Lesseq| Greater| Greatereq| Box_opaquehint not to open this formula
*)| Pseudo_de_bruijn of intmagic to embed De Bruijn indices in normal terms
*)| BCombBCIKS combinators
*)| CComb| IComb| KComb| SComb| Distinctinclude Interfaces.HASH with type t := tinclude Interfaces.EQ with type t := tinclude Interfaces.ORD with type t := tinclude Interfaces.PRINT with type t := tval is_prefix : t -> boolis_infix s returns true if the way the symbol is printed should be used in a prefix way if applied to 1 argument
val is_infix : t -> boolis_infix s returns true if the way the symbol is printed should be used in an infix way if applied to two arguments
val ty : t -> [ `Int | `Rat | `Other ]val mk_int : Logtk_arith.Z.t -> tval of_int : int -> tval int_of_string : string -> tval mk_rat : Logtk_arith.Q.t -> tval of_rat : int -> int -> tval rat_of_string : string -> tval is_int : t -> boolval is_rat : t -> boolval is_numeric : t -> boolval is_not_numeric : t -> boolval is_arith : t -> boolAny arithmetic operator, or constant
val is_logical_op : t -> boolAny arithmetic operator, or constant
val is_logical_binop : t -> boolval is_flattened_logical : t -> boolval is_quantifier : t -> boolval is_combinator : t -> boolval true_ : tval false_ : tval eq : tval neq : tval imply : tval equiv : tval xor : tval not_ : tval and_ : tval or_ : tval arrow : tval tType : tval prop : tval term : tval ty_int : tval ty_rat : tval ty_real : tval has_type : tval wildcard : t$_ for type inference
val multiset : ttype of multisets
val grounding : tval as_int : t -> intmodule Arith : sig ... endinclude Interfaces.ORD with type t := tmodule Map : Iter.Map.S with type key = tmodule Set : Iter.Set.S with type elt = tmodule Tag : sig ... endEach tag describes an extension of FO logic
Creates symbol and give them properties.
module TPTP : sig ... endThe module ArithOp deals only with numeric constants, i.e., all symbols must verify is_numeric (and most of the time, have the same type). The semantics of operations follows TPTP.
module ArithOp : sig ... endmodule ZF : sig ... end