Hunter Monroe
Results
3
comments of
Hunter Monroe
Understood, but it seems that a bullet/blurb is needed for each source, which can be combined into a list. Or more simply a toggle to include my language only for...
OK, so for Lean 4 itself, the file doc-gen-index.md would consist of: "Init is the initial code loaded by Lean 4 and is maintained in the github repository https://github.com/leanprover/lean4. Std...