Zulip Chat Archive

Stream: general

Topic: ext trace


view this post on Zulip Reid Barton (Sep 23 2019 at 17:25):

is there a way to get ext to print which lemmas it applied?

view this post on Zulip Simon Hudon (Sep 23 2019 at 17:32):

Not yet

view this post on Zulip Simon Hudon (Sep 23 2019 at 17:32):

Do you know how to implement it / do you have time to do it?

view this post on Zulip Reid Barton (Sep 23 2019 at 17:35):

I managed to guess the lemmas in the case I was looking at so it's not my problem any more :upside_down:

view this post on Zulip Simon Hudon (Sep 23 2019 at 17:37):

Blast! I'll try to make it harder next time :P

view this post on Zulip Reid Barton (Sep 23 2019 at 18:53):

On the subject of ext, it should probably complain if there are extra unused names. I found the ext intro x tactic in a line of mine which had been edited far too many times.

view this post on Zulip Simon Hudon (Sep 23 2019 at 19:03):

I don't see how the error message fixes that situation

view this post on Zulip Scott Morrison (Sep 23 2019 at 23:41):

ext intro x would introduce one new hypothesis, called intro, and then hopefully complain:
"hey, you gave me another hypothesis name, x, but I didn't find a use for it".

view this post on Zulip Scott Morrison (Sep 23 2019 at 23:42):

This actually should be pretty easy to do. A student here (@Lucas Allen) has some code that you can just wrap around another tactic, and it will produce strings of the form refine ... that reconstruct how the goal changed during the tactic invocation. Hopefully it could just be a matter of plugging that into ext?.

view this post on Zulip Scott Morrison (Sep 23 2019 at 23:45):

Hmm, I guess there are also the intros, which would require some extra handling. I agree this would be a desirable thing, so I created an issue #1481 to keep track of it. :-)

view this post on Zulip Simon Hudon (Sep 23 2019 at 23:57):

The issue with being inflexible like that is if the operands of = are of such a type as (a -> b) \x c. `ext will split that goal into two, the first goal can use another variable name but not the second.


Last updated: May 13 2021 at 06:15 UTC