package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = term
type builtin =
  1. | Prop
  2. | TType
  3. | Term
  4. | Int
  5. | Rat
type view =
  1. | Ty_builtin of builtin
  2. | Ty_var of t Var.t
  3. | Ty_app of ID.t * t list
  4. | Ty_fun of t list * t
  5. | Ty_forall of t Var.t * t
  6. | Ty_multiset of t
  7. | Ty_record of (string * t) list * t Var.t option
  8. | Ty_meta of meta_var
val view : t -> view
include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
val compare : t -> t -> int
val tType : t
val var : ?loc:location -> t Var.t -> t
val var_of_string : ?loc:location -> string -> t
val meta : ?loc:location -> meta_var -> t
val fun_ : ?loc:location -> t list -> t -> t
val app : ?loc:location -> ID.t -> t list -> t
val const : ?loc:location -> ID.t -> t
val forall : ?loc:location -> t Var.t -> t -> t
val forall_l : ?loc:location -> t Var.t list -> t -> t
val multiset : ?loc:location -> t -> t
val record : ?loc:location -> (string * t) list -> rest:t Var.t option -> t
val record_flatten : ?loc:location -> (string * t) list -> rest:t option -> t
val prop : t
val int : t
val rat : t
val real : t
val term : t
val (==>) : t list -> t -> t

Alias to fun_

val close_forall : t -> t
val unfold : t -> t Var.t list * t list * t

unfold [forall a b. x y z -> ret] returns the triples [a,b], [x,y,z], ret

val arity : t -> int * int

arity ty returns (n,m) where ty = forall x1..xn (a1 ... am -> ret)

val mangle : t -> string

String usable as an identifier, without whitespace

val needs_args : t -> bool

needs_args ty means that arity ty <> (0,0)

val is_tType : t -> bool
val is_prop : t -> bool
val returns : t -> t
val returns_tType : t -> bool
val returns_prop : t -> bool