Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: Using the `vm` monad
Eric Wieser (Oct 25 2021 at 11:47):
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 (Oct 25 2021 at 11:59):
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.
Eric Wieser (Oct 25 2021 at 12:29):
No I have no idea, I just found vm.get_decl before tactic.get_decl
Eric Wieser (Oct 25 2021 at 12:40):
Sorry, I said that wrong; my declaration has type vm_decl → option name, but I need to obtain a vm_decl somehow
Eric Wieser (Oct 25 2021 at 12:41):
So I want to call vm.get_decl, and have no idea how to
Gabriel Ebner (Oct 25 2021 at 12:49):
That is my point, you should avoid that part of Lean.
Eric Wieser (Oct 25 2021 at 12:50):
Fair, I think I've now found a better place for the new definition
Last updated: Dec 20 2023 at 11:08 UTC