Documentation

Mathlib.Tactic.GCongr.ForwardAttr

Environment extension for the forward-reasoning part of the gcongr tactic #

source
🔶 coverage
structure Mathlib.Tactic.GCongr.ForwardExt :
Type

An extension for gcongr_forward.

  • eval (h : Lean.Expr) (goal : Lean.MVarId) : Lean.MetaM Unit
Instances For
    source
    🔸 coverage
    def Mathlib.Tactic.GCongr.mkForwardExt (n : Lean.Name) :
    Lean.ImportM ForwardExt

    Read a gcongr_forward extension from a declaration of the right type.

    Instances For
      source
      🔸 coverage
      opaque Mathlib.Tactic.GCongr.forwardExt :
      Lean.PersistentEnvExtension Lean.Name (Lean.Name × ForwardExt) (List Lean.Name × List (Lean.Name × ForwardExt))

      Environment extensions for gcongrForward declarations