package logtk

  1. Overview
  2. Docs
On This Page
  1. Terms For Proofs
Core types and algorithms for logic

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

1.6.tar.gz
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d

doc/logtk.proofs/Logtk_proofs/LLTerm/index.html

Module Logtk_proofs.LLTermSource

Terms For Proofs

Sourcetype t
Sourcemodule Int_op : sig ... end
Sourcemodule Rat_op : sig ... end
Sourcetype 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 Z.t linexp * Int_op.t
  10. | Rat_pred of Q.t linexp * Rat_op.t
Sourceand 'a linexp

linear expression with coeffs of type 'a

Sourcetype term = t
Sourcetype ty = t
Sourcemodule type LINEXP = sig ... end

linear expressions

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

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

Sourceval pp_inner : t CCFormat.printer
Sourcemodule Form : sig ... end
Sourcemodule Set : CCSet.S with type elt = t
Sourcemodule Conv : sig ... end