ext trace

Stream: general

[Reid Barton]

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

[Simon Hudon]

Not yet

[Simon Hudon]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Scott Morrison]

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]

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]

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]

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.