HepLean Documentation

Mathlib.Tactic.GCongr.ForwardAttr

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

source
structure Mathlib.Tactic.GCongr.ForwardExt :
Type

An extension for gcongr_forward.

Instances For
    source
    def Mathlib.Tactic.GCongr.mkForwardExt (n : Lean.Name) :
    Lean.ImportM Mathlib.Tactic.GCongr.ForwardExt

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      opaque Mathlib.Tactic.GCongr.forwardExt :
      Lean.PersistentEnvExtension Lean.Name (Lean.Name × Mathlib.Tactic.GCongr.ForwardExt) (List Lean.Name × List (Lean.Name × Mathlib.Tactic.GCongr.ForwardExt))

      Environment extensions for gcongrForward declarations