package libzipperposition

  1. Overview
  2. Docs
On This Page
  1. Registration
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type
module C : module type of Env.C
type decl
val pp_decl : decl CCFormat.printer
type declare_result =
  1. | New of decl
  2. | 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