Def Lean.Name.isInternal'

Modification history

2023-12-28 17:56
Mathlib/Lean/Expr/Basic.lean
chore: remove `Name.isInternal'` in favour of `Name.isInternalDetail` (#9196) …
Deleted Lean.Name.isInternal'View on Github →
2023-03-08 15:13
Mathlib/Lean/Expr/Basic.lean
feat: initialize_simps_projections automatically finds coercions (#2045) …
Added Lean.Name.isInternal'View on Github →