Environment extensions for the inclusion tactic

This file defines the environment extensions used in the inclusion tactic.

structure Inclusion.InclusionExt : Type

An extension used by the inclusion tactic to construct ExprInclusionBodys.

• declName : Lean.Name

  Name of the declaration of the extension.

• family : Lean.Name

  The family in which the extension is registered.

• userName : Lean.Name

  The user-facing name of the extension.

• derive (e : Lean.Expr) : InclusionM ExprInclusionBody

  Attempt to construct an ExprInclusionBody for e.

• priority : Nat

  The priority of the extension. Extensions with higher priority are tried first.

structure Inclusion.HypothesisExt : Type

An extension used by the inclusion tactic to construct inclusion hypotheses from local declarations.

• declName : Lean.Name

  Name of the declaration of the extension.

• family : Lean.Name

  The family in which the extension is registered.

• userName : Lean.Name

  The user-facing name of the extension.

• derive (h : Lean.Expr) : HypothesisM Unit

  Attempt to construct inclusion hypotheses from h.

• priority : Nat

  The priority of the extension. Extensions with higher priority are tried first.

structure Inclusion.InclusionFamily : Type

A family of inclusion and hypothesis extensions.

• ref : Lean.Name

  The declaration the family was registered in. Recorded so that modules referring to the family by name still depend on the module registering it.

• inclusionExt : DiscrTreeExt.EnvExt InclusionExt

  The DiscrTree-indexed collection of inclusion extensions.

• hypothesisExt : DiscrTreeExt.EnvExt HypothesisExt

  The DiscrTree-indexed collection of hypothesis extensions.

instance Inclusion.instNonemptyInclusionFamily : Nonempty InclusionFamily

@[reducible, inline]

abbrev Inclusion.InclusionFamilies : Type

A map from family names to registered inclusion families.

Equations

• Inclusion.InclusionFamilies = Std.HashMap Lean.Name Inclusion.InclusionFamily

opaque Inclusion.inclusionFamiliesRef : IO.Ref InclusionFamilies

The registry of inclusion families.

def Inclusion.registerInclusionFamily (name : Lean.Name) (ref : Lean.Name := by exact decl_name%) : IO InclusionFamily

Register an inclusion family.

ref must name the declaration whose initializer runs the registration: it is what getInclusionFamily? records, so that a module naming the family acquires a dependency on the module registering it. The decl_name% default is correct for the usual initialize _ : InclusionFamily ← registerInclusionFamily .. idiom.

Equations

• One or more equations did not get rendered due to their size.

def Inclusion.getInclusionFamily? (name : Lean.Name) : Lean.CoreM (Option InclusionFamily)

If name is the name of an InclusionFamily family then return some family, otherwise return none.

Equations

• One or more equations did not get rendered due to their size.

def Inclusion.getInclusionFamily (name : Lean.Name) : Lean.CoreM InclusionFamily

Return the registered inclusion family named name, or fail if it is not registered.

Equations

• One or more equations did not get rendered due to their size.

def Inclusion.getInclusionExtMatches (families : Array Lean.Name) (e : Lean.Expr) : Lean.MetaM (Array InclusionExt)

Return an array of the inclusion extensions in families whose DiscrTree key matches e, sorted in order of highest to lowest priority.

Equations

• One or more equations did not get rendered due to their size.

def Inclusion.getHypothesisExtMatches (families : Array Lean.Name) (e : Lean.Expr) : Lean.MetaM (Array HypothesisExt)

Return an array of the hypothesis extensions in families whose DiscrTree key matches e, sorted in order of highest to lowest priority.

Equations

• One or more equations did not get rendered due to their size.

structure Inclusion.InclusionParamDecl : Type

A registered named parameter that can be set by the user and used across inclusion and hypothesis extensions.

• name : Lean.Name

  The name of the parameter.

• type : Lean.Expr

  The type of the parameter (as an expression).

• defaultValue? : Option Lean.Expr

  The default value of the parameter, if present.

@[reducible, inline]

abbrev Inclusion.InclusionParams : Type

The collection of registered inclusion parameters, indexed by name.

Equations

• Inclusion.InclusionParams = Lean.NameMap Inclusion.InclusionParamDecl

def Inclusion.mkInclusionParamDecl (name : Lean.Name) : Lean.ImportM InclusionParamDecl

Evaluate the declaration n as an InclusionParamDecl.

Equations

• Inclusion.mkInclusionParamDecl name = do let __x ← read match __x with | { env := env, opts := opts } => liftM (IO.ofExcept (Inclusion.mkInclusionParamDecl.unsafe_impl_2✝ name env opts))

opaque Inclusion.inclusionParamExt : Lean.ScopedEnvExtension Lean.Name (Lean.Name × InclusionParamDecl) InclusionParams

Initialize the InclusionParamExt environment extension.