Using the `vm` monad

Stream: general

[Eric Wieser]

In https://github.com/leanprover-community/lean/pull/638 I've added a new builtin definition of type vm name; how do I write a test for it? I can't seem to use the vm monad in a tactic block.

[Gabriel Ebner]

Are you sure you want to use the vm monad? As far as I remember, this was only ever used for a tiny debugger demo.