module Ind_cst:sig
..end
Skolem constants of an inductive type, coversets, etc. required for
inductive reasoning.
type
t
Ind_cst.t
only.
For instance, a constant of type nat
should be equal to
s^n(0)
in any model.exception InvalidDecl of string
exception NotAnInductiveConstant of Logtk.ID.t
val id_as_cst : Logtk.ID.t -> t option
val id_as_cst_exn : Logtk.ID.t -> t
as_cst
NotAnInductiveConstant
if it failsval id_is_cst : Logtk.ID.t -> bool
val on_new_cst : t Logtk.Signal.t
val make_skolem : Logtk.Type.t -> Logtk.ID.t
val make : ?depth:int -> is_sub:bool -> Logtk.Type.t -> t
val is_sub : t -> bool
val id_is_sub : Logtk.ID.t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val id : t -> Logtk.ID.t
val to_term : t -> Logtk.FOTerm.t
val ty : t -> Logtk.Type.t
val same_type : t -> t -> bool
val pp : t CCFormat.printer
val depth : t -> int
val dominates : t -> t -> bool
dominates c1 c2
if depth c1 < depth c2
. This way, in coversets,
the top constant dominates all sub-constantsmodule Cst_set:CCSet.S
with type elt = t
typeind_skolem =
Logtk.ID.t * Logtk.Type.t
val ind_skolem_compare : ind_skolem -> ind_skolem -> int
val ind_skolem_equal : ind_skolem -> ind_skolem -> bool
val id_is_ind_skolem : Logtk.ID.t -> Logtk.Type.t -> bool
id_is_potential_cst id ty
returns true
if id:ty
is
a skolem constant of an inductive type, or
if it is already an inductive constant.val find_ind_skolems : Logtk.FOTerm.t -> ind_skolem Sequence.t
find_ind_skolem term
searches subterms of term
for constants
that are of an inductive type and that are skolems or
(already) inductive constants.val ind_skolem_depth : Logtk.ID.t -> int