lean code block and variable command

[lecopivo]

Code block ```lean ... ``` and inline {lean}`...` does not see identifiers introduced by variable command.

For inline code, I'm suspecting that Elab.Term.elabTerm stx none is missing some version of runTermElabM.
I'm expecting that this should work

      discard <| Lean.Elab.Command.runTermElabM (fun _ => Elab.Term.elabTerm stx none)

but there is no lift from CommandElabM to DocElabM

mwe where import DemoTextbook.Exts.Exercises should probably be replaces with import Manual.Meta:

import Verso.Genre.Manual
import DemoTextbook.Exts.Exercises
open Verso.Genre Manual

open DemoTextbook.Exts (lean)

variable (X : Type)

#doc (Manual) "Test" =>

Array {lean}`Array X`

```lean
#check X
```

[david-christiansen]

This seems to be a bug with the reference manual code, rather than the contents of this one.

In any case, I believe I just pushed a fix over there:

It does require that the variable commands be in code blocks. This isn't ideal, but it's what I can make happen at just this moment.