package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TypedSTerm.TySource

Sourcetype t = term
Sourcetype builtin =
  1. | Prop
  2. | TType
  3. | Term
  4. | Int
  5. | Rat
Sourcetype 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
Sourceval view : t -> view
include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
include Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
Sourceval tType : t
Sourceval var : ?loc:location -> t Var.t -> t
Sourceval var_of_string : ?loc:location -> string -> t
Sourceval meta : ?loc:location -> meta_var -> t
Sourceval fun_ : ?loc:location -> t list -> t -> t
Sourceval app : ?loc:location -> ID.t -> t list -> t
Sourceval const : ?loc:location -> ID.t -> t
Sourceval forall : ?loc:location -> t Var.t -> t -> t
Sourceval forall_l : ?loc:location -> t Var.t list -> t -> t
Sourceval multiset : ?loc:location -> t -> t
Sourceval record : ?loc:location -> (string * t) list -> rest:t Var.t option -> t
Sourceval record_flatten : ?loc:location -> (string * t) list -> rest:t option -> t
Sourceval prop : t
Sourceval int : t
Sourceval rat : t
Sourceval real : t
Sourceval term : t
Sourceval (==>) : t list -> t -> t

Alias to fun_

Sourceval close_forall : t -> t
Sourceval 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

Sourceval arity : t -> int * int

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

Sourceval mangle : t -> string

String usable as an identifier, without whitespace

Sourceval needs_args : t -> bool

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

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