Module Ind_cst

module Ind_cst: sig .. end

Inductive Constants and Cases

Skolem constants of an inductive type, coversets, etc. required for inductive reasoning.

type t 
A ground term of an inductive type. It must correspond to a term built with the corresponding 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
Unsafe version of as_cst
Raises NotAnInductiveConstant if it fails
val id_is_cst : Logtk.ID.t -> bool
Check whether the given constant is an inductive constant
val on_new_cst : t Logtk.Signal.t
Triggered with new inductive constants
val make_skolem : Logtk.Type.t -> Logtk.ID.t
val make : ?depth:int -> is_sub:bool -> Logtk.Type.t -> t
Make a new constant of the given type
val is_sub : t -> bool
Is the constant a sub-constant (i.e. a subterm of a case in a coverset)?
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.Term.t
val ty : t -> Logtk.Type.t
val same_type : t -> t -> bool
Do these two inductive constants have the same type?
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-constants
module Cst_set: CCSet.S  with type elt = t
Set of constants

Inductive Skolems

type ind_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.Term.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
depth of the skolem (0 if not an inductive constant)