Module Sidekick_base.Uconst

Uninterpreted constants

type t = Types_.uconst = {
  1. uc_id : ID.t;
  2. uc_ty : ty;
}
val id : t -> ID.t
val ty : t -> ty
type Sidekick_core.Const.view += private
  1. | Uconst of t
include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.ORD with type t := t
val compare : t -> t -> int
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t
val const_decoders : Sidekick_core.Const.decoders
val make : ID.t -> ty -> t

Make a new uninterpreted function.

val uconst_of_id' : Sidekick_core.Term.store -> ID.t -> ty list -> ty -> Sidekick_core.Term.t
val uconst_of_str : Sidekick_core.Term.store -> string -> ty list -> ty -> Sidekick_core.Term.t
module Map : CCMap.S with type key = t
module Tbl : CCHashtbl.S with type key = t