mathlib
b651c6f6 - feat(tactic/core): add `run_parser` user command (#4745)

Commit
5 years ago
feat(tactic/core): add `run_parser` user command (#4745) Allows for writing things like: ```lean import tactic.core run_parser emit_code_here "def foo := 1" ``` Relevant Zulip conversation: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/universes/near/214229509
Author
Parents
Loading