Module type `EnumTypes.S`

module Env : Libzipperposition.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 -> 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.

returns: either the new declaration, or the already existing one for this type if any

raises Error: if some of the preconditions is not filled

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: Register rules in the environment