## Stream: general

### Topic: Official library note reference syntax

#### Gabriel Ebner (May 18 2020 at 18:51):

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 (May 18 2020 at 18:55):

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

#### Gabriel Ebner (May 18 2020 at 19:04):

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

#### Rob Lewis (May 18 2020 at 19:05):

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 (May 18 2020 at 19:06):

Do the docs check that the note actually exists?

#### Rob Lewis (May 18 2020 at 19:09):

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

#### Rob Lewis (May 19 2020 at 10:58):

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.

Last updated: May 13 2021 at 00:41 UTC