Mathlib.Tactic.GCongr.ForwardAttr

Mathlib.Tactic.GCongr.ForwardExt structure

Full source

/-- An extension for `gcongr_forward`. -/
structure ForwardExt where
  eval (h : Expr) (goal : MVarId) : MetaM Unit

Forward-reasoning extension for gcongr tactic

Informal description

A structure representing an extension for the forward-reasoning component of the `gcongr` tactic in Lean's Mathlib. This extension is used to enhance the capabilities of the `gcongr_forward` tactic.

Mathlib.Tactic.GCongr.mkForwardExt definition

(n : Name) : ImportM ForwardExt

Full source

/-- Read a `gcongr_forward` extension from a declaration of the right type. -/
def mkForwardExt (n : Name) : ImportM ForwardExt := do
  let { env, opts, .. } ← read
  IO.ofExcept <| unsafe env.evalConstCheck ForwardExt opts ``ForwardExt n

Construction of forward-reasoning extension for gcongr tactic

Informal description

The function `mkForwardExt` constructs a forward-reasoning extension for the `gcongr` tactic from a given declaration name. It evaluates the declaration in the current environment to produce an extension of type `ForwardExt`.

Mathlib.Tactic.GCongr.forwardExt opaque

: PersistentEnvExtension Name (Name × ForwardExt) (List Name × List (Name × ForwardExt))

Full source

/-- Environment extensions for `gcongrForward` declarations -/
initialize forwardExt : PersistentEnvExtension Name (Name × ForwardExt)
    (List Name × List (Name × ForwardExt)) ←
  registerPersistentEnvExtension {
    mkInitial := pure ([], {})
    addImportedFn := fun s => do
      let dt ← s.foldlM (init := {}) fun dt s => s.foldlM (init := dt) fun dt n => do
        return (n, ← mkForwardExt n) :: dt
      pure ([], dt)
    addEntryFn := fun (entries, s) (n, ext) => (n :: entries, (n, ext) :: s)
    exportEntriesFn := fun s => s.1.reverse.toArray
  }

Persistent Environment Extension for `gcongr` Forward-Reasoning

Informal description

The `forwardExt` is a persistent environment extension that maintains a collection of names paired with their corresponding `ForwardExt` structures, used for the forward-reasoning component of the `gcongr` tactic. It stores both a list of names and a list of name-extension pairs.