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)