diff --git a/.vscode/module-docstring.code-snippets b/.vscode/module-docstring.code-snippets new file mode 100644 index 0000000000000..9d1ed00c162b4 --- /dev/null +++ b/.vscode/module-docstring.code-snippets @@ -0,0 +1,35 @@ +{ + "Module docstring for mathlib": { + "scope": "lean", + "prefix": "module docstring", + "body": [ + "/-!", + "# ${TM_FILENAME_BASE/([^_]*)(_?)/${1:/capitalize}${2:+ }/g}", + "", + "## Main definitions", + "", + "* `foo_bar`", + "", + "## Main statements", + "", + "* `foo_bar_unique`", + "", + "## Notation", + "", + "", + "", + "## Implementation details", + "", + "", + "", + "## References", + "", + "* [F. Bar, *Quuxes*][bibkey]", + "", + "## Tags", + "", + "Foobars, barfoos", + "-/", + "", + ]}, +}