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

structure Mathlib.Tactic.GCongr.ForwardExt : Type

• eval : Lean.Expr → Lean.MVarId → Lean.MetaM Unit

An extension for gcongr_forward.

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

• Mathlib.Tactic.GCongr.mkForwardExt n = do let __discr ← read match __discr with | { env := env, opts := opts } => liftM (IO.ofExcept (Mathlib.Tactic.GCongr.mkForwardExt.impl✝ n env opts))

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