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