Zulip Chat Archive

Stream: general

Topic: extract_goal


view this post on Zulip Johan Commelin (May 29 2020 at 18:07):

Can we "Try this"-ify extract_goal? We can't use "Try this" immediately, I think, because we want to put the generated lemma before the current lemma and replace extract_goal foobar with apply foobar.

view this post on Zulip Johan Commelin (May 29 2020 at 18:07):

So we would need to do 2 replacements in one go.


Last updated: May 13 2021 at 17:42 UTC