Module LogtkHOTerm.TPTP

module TPTP: sig .. end

include LogtkInterfaces.PRINT
include LogtkInterfaces.PRINT_DE_BRUIJN
val true_ : LogtkHOTerm.t
tautology term
val false_ : LogtkHOTerm.t
antilogy term
val not_ : LogtkHOTerm.t
val and_ : LogtkHOTerm.t
val or_ : LogtkHOTerm.t
val imply : LogtkHOTerm.t
val equiv : LogtkHOTerm.t
val xor : LogtkHOTerm.t
val forall : LogtkHOTerm.t
val exists : LogtkHOTerm.t
val eq : LogtkHOTerm.t
val neq : LogtkHOTerm.t
val forall : LogtkHOTerm.t
val exists : LogtkHOTerm.t
val mk_forall : LogtkHOTerm.t list -> LogtkHOTerm.t -> LogtkHOTerm.t
val mk_exists : LogtkHOTerm.t list -> LogtkHOTerm.t -> LogtkHOTerm.t
val mk_not : LogtkHOTerm.t -> LogtkHOTerm.t
val mk_and : LogtkHOTerm.t -> LogtkHOTerm.t -> LogtkHOTerm.t
val mk_or : LogtkHOTerm.t -> LogtkHOTerm.t -> LogtkHOTerm.t
val mk_imply : LogtkHOTerm.t -> LogtkHOTerm.t -> LogtkHOTerm.t
val mk_equiv : LogtkHOTerm.t -> LogtkHOTerm.t -> LogtkHOTerm.t
val mk_xor : LogtkHOTerm.t -> LogtkHOTerm.t -> LogtkHOTerm.t
val mk_eq : LogtkHOTerm.t -> LogtkHOTerm.t -> LogtkHOTerm.t
val mk_neq : LogtkHOTerm.t -> LogtkHOTerm.t -> LogtkHOTerm.t
val mk_and_list : LogtkHOTerm.t list -> LogtkHOTerm.t
val mk_or_list : LogtkHOTerm.t list -> LogtkHOTerm.t
val close_forall : LogtkHOTerm.t -> LogtkHOTerm.t
Bind all free variables with 'forall'
val close_exists : LogtkHOTerm.t -> LogtkHOTerm.t
Bind all free variables with 'exists'
val __mk_forall : varty:LogtkType.t -> LogtkHOTerm.t -> LogtkHOTerm.t
val __mk_exists : varty:LogtkType.t -> LogtkHOTerm.t -> LogtkHOTerm.t