package logtk

  1. Overview
  2. Docs
On This Page
  1. Terms For Proofs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Terms For Proofs

type t
type var = t Logtk.HVar.t
module Int_op : sig ... end
module Rat_op : sig ... end
type view =
  1. | Type
  2. | Const of Logtk.ID.t
  3. | App of t * t
    (*

    curried application

    *)
  4. | Arrow of t * t
    (*

    functional arrow

    *)
  5. | Var of var
    (*

    bound var

    *)
  6. | Bind of {
    1. binder : Logtk.Binder.t;
    2. ty_var : t;
    3. body : t;
    }
  7. | AppBuiltin of Logtk.Builtin.t * t list
  8. | Ite of t * t * t
  9. | Int_pred of Logtk_arith.Z.t linexp * Int_op.t
  10. | Rat_pred of Logtk_arith.Q.t linexp * Rat_op.t
and 'a linexp

linear expression with coeffs of type 'a

type term = t
type ty = t
module type LINEXP = sig ... end

linear expressions

module Linexp_int : LINEXP with type num = Logtk_arith.Z.t
module Linexp_rat : LINEXP with type num = Logtk_arith.Q.t
val view : t -> view
val ty : t -> ty option
val ty_exn : t -> ty
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val is_type : t -> bool
val t_type : ty
val var : var -> t
val const : ty:ty -> Logtk.ID.t -> t
val app : t -> t -> t
val app_l : t -> t list -> t
val arrow : t -> t -> t
val arrow_l : t list -> t -> t
val bind : ty:ty -> Logtk.Binder.t -> ty_var:ty -> t -> t
val app_builtin : ty:ty -> Logtk.Builtin.t -> t list -> t
val builtin : ty:ty -> Logtk.Builtin.t -> t
val ite : t -> t -> t -> t
val int_pred : Linexp_int.t -> Int_op.t -> t
val rat_pred : Linexp_rat.t -> Rat_op.t -> t
val bool : ty
val box_opaque : t -> t
val lambda : ty_var:ty -> t -> t
val db_eval : sub:t -> t -> t

db_eval ~sub t replaces De Bruijn 0 in t by sub

val pp_inner : t CCFormat.printer
module Form : sig ... end
module Set : CCSet.S with type elt = t
module Conv : sig ... end
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