Functor EnumTypes.Make

module Make: functor (E : Env.S) -> S  with module Env = E

Parameters:

E : Env.S

module Env: Env.S

module C: module type of Env.C

type decl

val pp_decl : decl CCFormat.printer

type declare_result =

`\|`	`New of decl`
`\|`	`AlreadyDeclared of decl`

val declare_ty : proof:Logtk.Proof.t ->
       ty_id:Logtk.ID.t ->
       ty_vars:Logtk.Type.t Logtk.HVar.t list ->
       var:Logtk.Type.t Logtk.HVar.t ->
       EnumTypes.term list -> declare_result

Declare that the domain of the type ty_id is restricted to given list of cases, in the form forall var. Or_{c in cases} var = c. The type of var must be ty_id ty_vars. Will be ignored if the type already has a enum declaration, and the old declaration will be returned instead.
Raises Error if some of the preconditions is not filled
Returns either the new declaration, or the already existing one for this type if any

val instantiate_vars : Env.multi_simpl_rule

Instantiate variables whose type is a known enumerated type, with all cases of this type.

Registration

val setup : unit -> unit