Module EnumTypes.Make

Parameters

E : Libzipperposition.Env.S

Signature

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.