Johan Commelin (Feb 03 2020 at 16:04):
I tried to put a codeblock as in
```lean foo ```
in a docstring. But I got a complaint, so I removed it: https://github.com/leanprover-community/mathlib/pull/1946/commits/48a5d7c99a83709e5736398db58ef39fb4bc0821#diff-e43627ca2566b806fcd077fad0fe29c9L26
If you don't add the
lean tag, then everything is fine. So
``` foo ```
works fine. I can imagine that the language modifier might be useful. But it isn't crucial. Just posting to see what others think.
Johan Commelin (Feb 03 2020 at 16:05):
FYI: the error that Lean gave was
invalid docstring: expected end of code block, or something like that.
Bryan Gin-ge Chen (Feb 03 2020 at 16:14):
Looks like the error message comes from the code around here, so we could update that in 3.5.x to ignore such tags.
Rob Lewis (Feb 03 2020 at 16:15):
It's handled correctly here: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/reassoc_axiom.lean#L15
Yury G. Kudryashov (Feb 03 2020 at 16:19):
What's the difference?
Bryan Gin-ge Chen (Feb 03 2020 at 16:25):
I guess there's a bug somewhere. This gives the invalid docstring error:
/-! ```lean a ``` a -/
/-! ```lean a ``` -/
Neither does this (though it should):
/-! ```lean a ``` ``` -/
Bryan Gin-ge Chen (Feb 03 2020 at 18:30):
This is now issue 108 on leanprover-community/lean. I probably won't be able to look at this any more for now.
Bryan Gin-ge Chen (Feb 14 2020 at 03:20):
I looked at this again. The issue that @Johan Commelin pointed out was actually fixed last year in this PR which was merged into 3.5.0.
However, this example:
/-! ``` ``` ``` -/
does not throw an error, even though it should.
Last updated: May 15 2021 at 23:13 UTC