Zulip Chat Archive

Stream: general

Topic: from tactics to terms


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Aug 24 2018 at 13:22):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Aug 24 2018 at 13:53):

You'll need to trace it?

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Aug 24 2018 at 14:02):

sounds ironic

view this post on Zulip Kevin Buzzard (Aug 24 2018 at 14:53):

trace_state usually prints a trace.

view this post on Zulip Sebastian Ullrich (Aug 24 2018 at 15:35):

@Johan Commelin See tactic.trace_result


Last updated: May 14 2021 at 07:19 UTC