package logtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val true_ : t
val false_ : t
val atom : term -> t
val not_ : t -> t
val and_ : t list -> t
val or_ : t list -> t
val imply : t -> t -> t
val equiv : t -> t -> t
val xor : t -> t -> t
val eq : term -> term -> t
val neq : term -> term -> t
val mk_eq : bool -> term -> term -> t
val mk_atom : bool -> term -> t

Quantifiers: the term list must be a list of free variables.

val forall : term list -> t -> t
val exists : term list -> t -> t
val forall_ty : type_ list -> t -> t
val __mk_forall : varty:type_ -> t -> t
val __mk_exists : varty:type_ -> t -> t
val __mk_forall_ty : t -> t