Missing library notes

Stream: mathlib4

[Anne Baanen]

I can't find the declaration of the "lower instance priority" library note. In fact, grep only counts 27 occurrences of library_note in the mathlib4 repo (excluding the command setup itself) while it counts 37 in mathlib3 (again excluding the command setup itself).

[Eric Wieser]

Maybe an old version of mathport didn't support them, and so they're missing from early files?

[Eric Wieser]

Or more concerningly, maybe we have 10 ad-hoc files at the root of the import tree that were not ported at all

[Anne Baanen]

Sadly the syntax is slightly different so here is my best attempt at a manual diff (< marks lines only found in Mathlib 3, > only in Mathlib 4):

McChouffe% diff <(sort ../library-note-3) <(sort ../library-note-4)
1,16c1,7
< library_note "category_theory universes"
---
> library_note "CategoryTheory universes"
25,62c16,31
< library_note "function coercion"
< library_note "implicit instance arguments"
< library_note "is_R_or_C instance"
< library_note "likely generated binder names"
< library_note "lower instance priority"
< library_note "nolint_ge"
< library_note "open expressions"
< library_note "open expressions"
< library_note "partially-applied ext lemmas"
< library_note "use has_coe_t"
< library_note "user attribute parameters"
---
> library_note "IsROrC instance"/--
> library_note "norm_num lemma function equality"/--

Probably most of these are correctly removed because they are Lean 3 specific and I spot two renames, but we should check that carefully.

[Scott Morrison]

While not forgetting to followup on checking these library notes carefully, let me note the two open issues about clickability of library notes:

• https://github.com/leanprover/vscode-lean4/issues/286
• https://github.com/leanprover/doc-gen4/issues/135