package libzipperposition

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

Module Libzipperposition_calculi.App_encodeSource

Applicative Encoding

Sourceval section : Logtk.Util.Section.t
Sourceval mode_ : [ `Extensional | `Intensional | `None ] ref
Sourcemodule T = Logtk.TypedSTerm
Sourceval id_ae_fun : Logtk.ID.t
Sourceval ty_ae_fun : T.t
Sourceval function_type : T.t
Sourceval id_ae_app : Logtk.ID.t
Sourceval ty_ae_app : T.t
Sourceval const_ae_app : T.t
Sourceval ty_decls : (Logtk.Cnf.clause, T.t, T.t) Logtk.Statement.t Iter.t

Type declarations for these new symbols

Sourceval app_encode_ty : T.t -> T.t

Encode a type

Sourceval is_type : T.t -> bool

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

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

Encode a variable

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

Encode a term

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

Encode a literal

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

Encode a clause

Sourceexception E_i of (T.t Logtk.SLiteral.t list, T.t, T.t) Logtk.Statement.t
Sourceval pp_in : 'a CCFormat.printer -> 'b CCFormat.printer -> 'c CCFormat.printer -> Logtk.Output_format.t -> ('a, 'b, 'c) Logtk.Statement.t CCFormat.printer
Sourceval pp_clause_in : Logtk.Output_format.t -> (T.t Logtk.SLiteral.t list, T.t, T.t) Logtk.Statement.t CCFormat.printer
Sourceval result_tc : (T.t Logtk.SLiteral.t list, T.t, T.t) Logtk.Statement.t Logtk.Proof.Result.tc
Sourceval app_encode_stmt : (T.t Logtk.SLiteral.t list, T.t, T.t) Logtk.Statement.t -> (T.t Logtk.SLiteral.t list, 'a, T.t) Logtk.Statement.t

encode a statement

Sourceval extensionality_axiom : (T.t Logtk.SLiteral.t list, T.t, T.t) Logtk.Statement.t
Sourceval 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