Mario Carneiro

I'm sure I'm not the only one who has written things like [this](https://github.com/digama0/mm0/blob/98496badaf6464e56ed7b4204e7d54b85667cb01/mm0-rs/src/doc/mod.rs#L513-L521): ```rust writeln!(w, " \ \ \n\ \n\ \n \ \n \ \n {h1}\ \n {nav}\ \n ")...

Incidentally, the PHP heredoc syntax solves the indentation issue by using the indentation of the *closing* quote character, rather than the first content line or the minimum indentation. Thus: ```rust...

> I really like the syntax except that typing it/pasting it in markdown itself is error-prone, since code can now close code blocks without being obvious. I think that for...

> I don’t mind dropping the `Theory` suffix though I wonder a bit about the way users will still need to remember it when they come to refer to the...

Notes from HOL meeting: ``` Theory thy[bare] (* Module documentation *) Ancestors long_name[alias LN, qualified, ignore_grammar] other[ignore_grammar] baz arithmetic list Libs preamble Theory fooLib listSyntax val _ = bazTheory.bla; Definition...

Can someone !bench this?

Also !bench for the control group (remove the optimization), since I suspect it is not getting hit in the first place, at least in the benchmark suite

@semorrison Do you know if it is possible to run a benchmark comparison on mathlib? (I would like to have the above two benchmarks on mathlib: the defeq switch and...

@semorrison Okay, I've removed the "control group" test from this PR and moved it to #2748.

I'm pretty sure the breakage is spurious; a lot of PRs are "breaking mathlib" because the bot merges master into the release PR, without compensating for this with the bump...