Zulip Chat Archive

Stream: general

Topic: ext trace


Reid Barton (Sep 23 2019 at 17:25):

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

Simon Hudon (Sep 23 2019 at 17:32):

Not yet

Simon Hudon (Sep 23 2019 at 17:32):

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

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:

Simon Hudon (Sep 23 2019 at 17:37):

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

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.

Simon Hudon (Sep 23 2019 at 19:03):

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

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".

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?.

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. :-)

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: Dec 20 2023 at 11:08 UTC