Def Lean.Elab.Term.mkFreshLevelParam

Modification history

2026-03-21 05:43
Mathlib/Lean/Elab/Term.lean
chore: import `Type*` in `Mathlib.Init` (#36316) …
Modified Lean.Elab.Term.mkFreshLevelParamView on Github →
2025-12-01 19:09
Mathlib/Lean/Elab/Term.lean
feat(Mathlib/Tactic/CategoryStar): Category* (#30797) …
Added Lean.Elab.Term.mkFreshLevelParamView on Github →