## Stream: general

### 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 meta.

#### 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 trace it?

#### 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)


sounds ironic

#### 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 tactic.trace_result

Last updated: May 14 2021 at 07:19 UTC