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