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

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

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

Environment extensions for gcongrForward declarations