Official library note reference syntax

Stream: general

[Gabriel Ebner]

I've just been reading our CICM paper and wondering about the following passage:

When these notes are referenced in other documentation entries with the syntax Note [note name]

I was actually under the impression that the official syntax is see Note [note name], but I learned this from imitating usage in mathlib. The vscode extension currently expects the "see" at the beginning, should I change this?

[Rob Lewis]

Enforcing "see" can make it grammatically awkward and I don't think there's any need to...

[Gabriel Ebner]

Ok, I'll remove it. Is there anything else that parses the note [note name] syntax?

[Rob Lewis]

The docs do, but I think they're probably ignoring the "see" already. https://leanprover-community.github.io/mathlib_docs/notes.html#default%20priority

[Gabriel Ebner]

Do the docs check that the note actually exists?

[Rob Lewis]

Uh, I'm not sure, I'll check later.

[Rob Lewis]

Gabriel Ebner said:

Do the docs check that the note actually exists?

It does not. It just uses a built in markdown thing to linkify patterns.