Library for Zipperposition



module Env = E
module C : sig ... end
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.

val setup : unit -> unit

Register rules in the environment