Module LogtkPrologTerm.TPTP

module TPTP: sig .. end

TPTP constructors and printing

The constructors take the semantics of TPTP into consideration. In particular, wildcard (fresh variables) are inserted in front of ad-hoc polymorphic symbols such as eq or neq.


val true_ : LogtkPrologTerm.t
val false_ : LogtkPrologTerm.t
val var : ?loc:LogtkPrologTerm.location ->
?ty:LogtkPrologTerm.t -> string -> LogtkPrologTerm.t
val const : ?loc:LogtkPrologTerm.location -> LogtkSymbol.t -> LogtkPrologTerm.t
val app : ?loc:LogtkPrologTerm.location ->
LogtkPrologTerm.t -> LogtkPrologTerm.t list -> LogtkPrologTerm.t
val bind : ?loc:LogtkPrologTerm.location ->
LogtkSymbol.t ->
LogtkPrologTerm.t list -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val and_ : ?loc:LogtkPrologTerm.location -> LogtkPrologTerm.t list -> LogtkPrologTerm.t
val or_ : ?loc:LogtkPrologTerm.location -> LogtkPrologTerm.t list -> LogtkPrologTerm.t
val not_ : ?loc:LogtkPrologTerm.location -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val equiv : ?loc:LogtkPrologTerm.location ->
LogtkPrologTerm.t -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val xor : ?loc:LogtkPrologTerm.location ->
LogtkPrologTerm.t -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val imply : ?loc:LogtkPrologTerm.location ->
LogtkPrologTerm.t -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val eq : ?loc:LogtkPrologTerm.location ->
?ty:LogtkPrologTerm.t ->
LogtkPrologTerm.t -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val neq : ?loc:LogtkPrologTerm.location ->
?ty:LogtkPrologTerm.t ->
LogtkPrologTerm.t -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val forall : ?loc:LogtkPrologTerm.location ->
LogtkPrologTerm.t list -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val exists : ?loc:LogtkPrologTerm.location ->
LogtkPrologTerm.t list -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val lambda : ?loc:LogtkPrologTerm.location ->
LogtkPrologTerm.t list -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val mk_fun_ty : ?loc:LogtkPrologTerm.location ->
LogtkPrologTerm.t list -> LogtkPrologTerm.t -> LogtkPrologTerm.t
val tType : LogtkPrologTerm.t
val forall_ty : ?loc:LogtkPrologTerm.location ->
LogtkPrologTerm.t list -> LogtkPrologTerm.t -> LogtkPrologTerm.t
include LogtkInterfaces.PRINT