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
  6. | Real
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 for 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_quantifier_free : t -> bool

true iff it contains no "forall ty"

val is_prenex : t -> bool

true iff prenex quantification only

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct