Def Lean.Elab.Term.mkFreshLevelParam

Modification history

2025-12-01 19:09
Mathlib/Lean/Elab/Term.lean
feat(Mathlib/Tactic/CategoryStar): Category* (#30797) …
Added Lean.Elab.Term.mkFreshLevelParamView on Github →