Def Mathlib.Tactic.ClickSuggestions.hasUnhelpfulMVars

Modification history

2026-09-13 20:34
Mathlib/Tactic/ClickSuggestions/Util.lean
feat(ClickSuggestions): support assigning metavariables in the goal (#43597) …
Added Mathlib.Tactic.ClickSuggestions.hasUnhelpfulMVarsView on Github →