verso
verso copied to clipboard
leanprover
Lean documentation authoring tool
A recent blog post is 1.88 MB - that's too big! It's time to look into deduplicating some of the metadata that ends up in the generated code.
It would be nice if there was a function to support translation into other languages. The mdbook currently used for documentation does not support this.
For now, Verso supports inline math and display math but the latter can only use inline code block: ```` $`\sum_{i=0}^{10} i` $$`\sum_{i=0}^{10} i` ```` It doesn't seem possible to use...
I would like to ask a question about how users can use verso to write documents. 1A. When a user tries to write a document using the verso, do they...
While writing a blog post I was regularly confused by strange syntax errors (missing end of file), and multiple times it turned out I had ```` ```leanOutput foo some outupt...
RIght now, it's hard to figure out how to write a genre. It would be good to have a minimal example of a Verso genre, with comments, in the repository,...
Using ``` {include VersoTest.Introduction.Getting_Started} {include VersoTest.Introduction.Overview} ``` which misses a blank line turns up the unhelpful message: ``` unexpected syntax failed to pretty print term (use 'set_option pp.rawOnError true' for...
E.g.: ``` Here's a _thing ``` The error is just `'_'`, not `expected '_'`