package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

Applicative Encoding

val section : Logtk.Util.Section.t
val mode_ : [ `Extensional | `Intensional | `None ] ref
module T = Logtk.TypedSTerm
val id_ae_fun : Logtk.ID.t
val ty_ae_fun : T.t
val function_type : T.t
val id_ae_app : Logtk.ID.t
val ty_ae_app : T.t
val const_ae_app : T.t
val id_ext_diff : Logtk.ID.t
val ty_ext_diff : T.t
val const_ext_diff : T.t

Type declarations for these new symbols

val ty_decl_ext_diff : (Logtk.Cnf.clause, T.t, T.t) Logtk.Statement.t
val app_encode_ty : T.t -> T.t

Encode a type

val is_type : T.t -> bool

Is a term a type? i.e. is a term of type tType?

val app_encode_var : T.t Logtk.Var.t -> T.t Logtk.Var.t

Encode a variable

val app_encode_term : bool -> T.t -> T.t

Encode a term

val app_encode_lit : T.t Logtk.SLiteral.t -> T.t Logtk.SLiteral.t

Encode a literal

val app_encode_lits : T.t Logtk.SLiteral.t list -> T.t Logtk.SLiteral.t list

Encode a clause

exception E_i of (T.t Logtk.SLiteral.t list, T.t, T.t) Logtk.Statement.t

encode a statement

val extensionality_axiom : (T.t Logtk.SLiteral.t list, T.t, T.t) Logtk.Statement.t
val options : (string * [> `Extensional | `Intensional | `None ]) list
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