package libzipperposition

  1. Overview
  2. Docs
On This Page
  1. Cover Set
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
val ty : t -> Logtk.Type.t
val top : t -> cst

top constant of the coverset

val declarations : t -> (Logtk.ID.t * Logtk.Type.t) Iter.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:[ `Rec | `Base | `All ] -> t -> case Iter.t

Cases of the cover set

val sub_constants : t -> cst Iter.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.

  • parameter depth

    the induction depth for the top constant in the coverset

  • parameter cover_set_depth

    the depth of each case, that is, the number of constructor between the root of terms and leaf constants. default 1.