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