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 =
| Type
| Const of Logtk.ID.t
| App of t * t

curried application

| Arrow of t * t

functional arrow

| Var of var

bound var

| Bind of {
binder : Logtk.Binder.t;
ty_var : t;
body : t;
}
| AppBuiltin of Logtk.Builtin.t * t list
| Ite of t * t * t
| Int_pred of Z.t linexp * Int_op.t
| Rat_pred of Q.t linexp * Rat_op.t
type '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 = Z.t
module Linexp_rat : LINEXP with type num = 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 : t CCFormat.printer
val pp_inner : t CCFormat.printer
module Form : sig ... end
module Set : CCSet.S with type Set.elt = t
module Conv : sig ... end