Module Sidekick_core_logic.Const

Constants.

Constants are logical symbols, defined by the user thanks to an open type

type view = ..
module Ops : sig ... end
type t = {
  1. c_view : view;
  2. c_ops : Ops.t;
  3. c_ty : Sidekick_core_logic__.Types_.term;
}
val view : t -> view
val make : view -> Ops.t -> ty:Sidekick_core_logic__.Types_.term -> t
val ser : ser_t:(Sidekick_core_logic__.Types_.term -> Sidekick_util.Ser_value.t) -> t -> string * Sidekick_util.Ser_value.t
val ty : t -> Sidekick_core_logic__.Types_.term
type decoders = (string * Ops.t * (Sidekick_core_logic__.Types_.term Sidekick_util.Ser_decode.t -> view Sidekick_util.Ser_decode.t)) list

Decoders for constants: given a term store, return a list of supported tags, and for each tag, a decoder for constants that have this particular tag.

include Sidekick_sigs.EQ_HASH_PRINT with type t := t
include Sidekick_sigs.EQ with type t := t
val equal : t -> t -> bool
include Sidekick_sigs.HASH with type t := t
val hash : t -> int
include Sidekick_sigs.PRINT with type t := t