-
Notifications
You must be signed in to change notification settings - Fork 88
/
LibraryNote.lean
40 lines (34 loc) · 1 KB
/
LibraryNote.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
/-
Copyright (c) 2022 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner
-/
import Lean.Elab.ElabRules
/-!
# Define the `library_note` command.
-/
namespace Batteries.Util.LibraryNote
open Lean
/-- A library note consists of a (short) tag and a (long) note. -/
def LibraryNoteEntry := String × String
/-- Environment extension supporting `library_note`. -/
initialize libraryNoteExt : SimplePersistentEnvExtension LibraryNoteEntry (Array LibraryNoteEntry) ←
registerSimplePersistentEnvExtension {
addEntryFn := Array.push
addImportedFn := Array.concatMap id
}
open Lean Parser Command in
/--
```
library_note "some tag" /--
... some explanation ...
-/
```
creates a new "library note", which can then be cross-referenced using
```
-- See note [some tag]
```
in doc-comments.
-/
elab "library_note " title:strLit ppSpace text:docComment : command => do
modifyEnv (libraryNoteExt.addEntry · (title.getString, text.getDocString))