Previous  Up  Next

Module Builtin

module Builtin: sig .. end

Builtin Objects

Covers numbers, connectives, and builtin types
Since 1.0

type t =
| Not
| And
| Or
| Imply
| Equiv
| Xor
| Eq
| Neq
| HasType
| True
| False
| Arrow
| Wildcard
| Multiset
| TType
| Prop
| Term
| ForallConst (*
constant for simulating forall
*)
| ExistsConst (*
constant for simulating exists
*)
| TyInt
| TyRat
| Int of Z.t
| Rat of Q.t
| 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 
include Interfaces.HASH
include Interfaces.ORD
include Interfaces.PRINT
type fixity =
| Infix_binary
| Infix_nary
| Prefix 
val fixity : t -> fixity
val is_prefix : t -> bool
is_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 -> bool
is_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 | `Other | `Rat ]
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
type of multisets
module Arith: sig .. end
include Interfaces.HASH
include Interfaces.ORD
include Interfaces.PRINT
module Map: Sequence.Map.S  with type key = t
module Set: Sequence.Set.S  with type elt = t
module Tbl: Hashtbl.S  with type key = t

TPTP Interface

Creates symbol and give them properties.
module TPTP: sig .. end

The module Builtin.ArithOp deals only with numeric constants, i.e., all symbols must verify Builtin.is_numeric (and most of the time, have the same type). The semantics of operations follows TPTP.
module ArithOp: sig .. end

ZF


module ZF: sig .. end