Contributing

Discuss

GitHub Discussion is here. Feel free to correct mistakes, ask questions or share ideas.

Documentation

To compile this book, you need mdbook and some plugins.

• mdbook
• mdbook-katex for KaTeX

mdbook serve md

mdbook build md

But you don't have to install to simply correct mistakes and write documents, since it can be previewed by your editor's markdown preview.

Developing

VSCode settings

Some notation is not prepared default by lean 4 extension for VSCode. Here is example .vscode/settings.json.

{
  "lean4.input.customTranslations": {
    "cand": "⋏",
    "cor": "⋎",
    "boxdot": "⊡",
    "^F": "ꟳ"
  }
}