Def Mathlib.Tactic.GCongr.hasHoleAnnotation

Modification history

2025-11-13 17:14

Mathlib/Tactic/GCongr/Core.lean

feat(gcongr): use mdata instead of template (#30739) …

Added Mathlib.Tactic.GCongr.hasHoleAnnotation View on Github →