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.2.17@m4x.org

Sources

2.1.tar.gz
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

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

Module Logtk_proofs.LLTerm

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