module Cover_set:`sig`

..`end`

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