LRA_term (sidekick-base.Sidekick_base.LRA

module Pred : sig ... end

module Op : sig ... end

val const_decoders : Sidekick_core.Const.decoders

module View : sig ... end

type term = Sidekick_core.Term.t

type ty = Sidekick_core.Term.t

val term_of_view : Sidekick_core.Term.store -> term View.t -> term

val real : Sidekick_core.Term.store -> ty

val has_ty_real : term -> bool

val pred : Sidekick_core.Term.store -> Pred.t -> term -> term -> term

val mult_by : Sidekick_core.Term.store -> Q.t -> term -> term

val op : Sidekick_core.Term.store -> Op.t -> term -> term -> term

val const : Sidekick_core.Term.store -> Q.t -> term

val leq : Sidekick_core.Term.store -> term -> term -> term

val lt : Sidekick_core.Term.store -> term -> term -> term

val geq : Sidekick_core.Term.store -> term -> term -> term

val gt : Sidekick_core.Term.store -> term -> term -> term

val eq : Sidekick_core.Term.store -> term -> term -> term

val neq : Sidekick_core.Term.store -> term -> term -> term

val plus : Sidekick_core.Term.store -> term -> term -> term

val minus : Sidekick_core.Term.store -> term -> term -> term

val view : term -> term View.t

View as LRA