from tactics to terms

Stream: general

[Johan Commelin]

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]

Ok, I found format_result in Ed's recent docs on meta.

[Johan Commelin]

The problem is that I don't see any output anywhere, when I plug it into some begin ... end block.

[Scott Morrison]

You'll need to trace it?

[Johan Commelin]

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]

sounds ironic

[Kevin Buzzard]

trace_state usually prints a trace.

[Sebastian Ullrich]

@Johan Commelin See tactic.trace_result