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

structure Mathlib.Tactic.GCongr.ForwardExt : Type

An extension for gcongr_forward.

• eval (h : Lean.Expr) (goal : Lean.MVarId) : Lean.MetaM Unit

def Mathlib.Tactic.GCongr.mkForwardExt (n : Lean.Name) : Lean.ImportM 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.

opaque Mathlib.Tactic.GCongr.forwardExt : Lean.PersistentEnvExtension Lean.Name (Lean.Name × ForwardExt) (List Lean.Name × List (Lean.Name × ForwardExt))

Environment extensions for gcongrForward declarations