Topic: from tactics to terms
Johan Commelin (Aug 24 2018 at 07:48):
Even though I'm beginning to understand a bit of the
meta-world, I still don't fully comprehend the tactic monad. For example: is it possible to extract a concrete term from a
begin ... end-block?
Johan Commelin (Aug 24 2018 at 13:22):
Ok, I found
format_result in Ed's recent docs on
Johan Commelin (Aug 24 2018 at 13:28):
The problem is that I don't see any output anywhere, when I plug it into some
begin ... end block.
Scott Morrison (Aug 24 2018 at 13:53):
You'll need to
Johan Commelin (Aug 24 2018 at 14:01):
Hmm. Good idea. But
trace tactic.format_result gives the error
failed to synthesize type class instance for ⊢ has_to_tactic_format (tactic format)
Patrick Massot (Aug 24 2018 at 14:02):
Kevin Buzzard (Aug 24 2018 at 14:53):
trace_state usually prints a trace.
Sebastian Ullrich (Aug 24 2018 at 15:35):
@Johan Commelin See
Last updated: May 14 2021 at 07:19 UTC