Module Logtk.Builtin
Builtin Objects
type t
=
include Interfaces.PRINT with type t := t
val fixity : t -> fixity
val is_prefix : t -> bool
is_infix s
returnstrue
if the way the symbol is printed should be used in a prefix way if applied to 1 argument
val is_infix : t -> bool
is_infix s
returnstrue
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 : Z.t -> t
val of_int : int -> t
val int_of_string : string -> t
val mk_rat : Q.t -> t
val of_rat : int -> int -> t
val rat_of_string : string -> t
val is_int : t -> bool
val is_rat : t -> bool
val is_numeric : t -> bool
val is_not_numeric : t -> bool
val is_arith : t -> bool
Any arithmetic operator, or constant
val true_ : t
val false_ : t
val eq : t
val neq : t
val imply : t
val equiv : t
val xor : t
val not_ : t
val and_ : t
val or_ : t
val arrow : t
val tType : t
val prop : t
val term : t
val ty_int : t
val ty_rat : t
val has_type : t
val wildcard : t
$_ for type inference
val multiset : t
$_ for type inference
type of multisets
val grounding : t
module Arith : sig ... end
include Interfaces.PRINT with type t := t
module Tag : sig ... end
Each tag describes an extension of FO logic
TPTP Interface
Creates symbol and give them properties.
module TPTP : sig ... end
module ArithOp : sig ... end
ZF
module ZF : sig ... end