package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = private LogtkScopedTerm.t
val of_term : LogtkScopedTerm.t -> t option
val of_term_exn : LogtkScopedTerm.t -> t
val ty : t -> type_
val size : t -> int
include LogtkInterfaces.HASH with type t := t
include LogtkInterfaces.EQ with type t := t
val eq : t -> t -> bool
val hash_fun : t CCHash.hash_fun
val hash : t -> int
include LogtkInterfaces.ORD with type t := t
val cmp : t -> t -> int
module Seq : sig ... end
module Set : Sequence.Set.S with type elt = t
val to_prolog : ?depth:int -> t -> LogtkPrologTerm.t
include LogtkInterfaces.PRINT_DE_BRUIJN with type t := t and type term := t
type print_hook = int -> (Buffer.t -> t -> unit) -> Buffer.t -> t -> bool

User-provided hook that can be used to print terms (for composite cases) before the default printing occurs. The int argument is the De Bruijn depth in the term. A hook takes as arguments the depth and the recursive printing function that it can use to print subterms. A hook should return true if it fired, false to fall back on the default printing.

val pp_depth : ?hooks:print_hook list -> int -> Buffer.t -> t -> unit
val default_hooks : unit -> print_hook list
module TPTP : sig ... end