Module Cover_set

module Cover_set: sig .. end

Cover Set

Use for reasoning by case during induction
type cst = Ind_cst.t 
type term = Logtk.Term.t 
type case 
type t 
module Case: sig .. end
Inductive Case
val pp : t CCFormat.printer
val ty : t -> Logtk.Type.t
val top : t -> cst
top constant of the coverset
val declarations : t -> (Logtk.ID.t * Logtk.Type.t) Sequence.t
declarations set returns a list of type declarations that should be made if set is new (declare the top cst and its subcases)
val cases : ?which:[ `All | `Base | `Rec ] -> t -> case Sequence.t
Cases of the cover set
val sub_constants : t -> cst Sequence.t
All sub-constants of a given inductive constant
val make : ?cover_set_depth:int -> depth:int -> Logtk.Type.t -> t
Build a cover set for the given type.

a set of ground terms [t1,...,tn] with fresh constants inside (that are not declared as inductive!) such that bigor_{i in 1...n} t=ti is the skolemized version of the exhaustivity axiom on t's type.

cover_set_depth : the depth of each case, that is, the number of constructor between the root of terms and leaf constants. default 1.
depth : the induction depth for the top constant in the coverset