lean codeblocks in docstrings

Stream: general

[Johan Commelin]

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]

FYI: the error that Lean gave was invalid docstring: expected end of code block, or something like that.

[Bryan Gin-ge Chen]

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]

It's handled correctly here: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/reassoc_axiom.lean#L15

[Yury G. Kudryashov]

What's the difference?

[Bryan Gin-ge Chen]

I guess there's a bug somewhere. This gives the invalid docstring error:

/-!

```lean
a
```

a
-/

This doesn't:

/-!

```lean
a
```


-/

Neither does this (though it should):

/-!

```lean
a
```

```
-/

[Bryan Gin-ge Chen]

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]

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.