Zulip Chat Archive

Stream: general

Topic: rfunext


view this post on Zulip Johan Commelin (May 29 2020 at 13:58):

Do people want a rfunext tactic, that is to funext what rintro is to intro?

view this post on Zulip Kenny Lau (May 29 2020 at 13:59):

at this rate, next week we will have a tactic that applies machine learning to close the goal

view this post on Zulip Kenny Lau (May 29 2020 at 13:59):

and then the week after that we will have a tactic that uses machine learning to guess what theorems you want to prove

view this post on Zulip Johan Commelin (May 29 2020 at 14:00):

How about a tactic that uses machine learning to guess which tactics I want?

view this post on Zulip Johan Commelin (May 29 2020 at 14:02):

But seriously, rfunext should be a souped up version of funext >>= rintro. Only need some parser sugar.

view this post on Zulip Reid Barton (May 29 2020 at 14:03):

Do you mean ext?

view this post on Zulip Johan Commelin (May 29 2020 at 14:04):

rext?

view this post on Zulip Johan Commelin (May 29 2020 at 14:04):

I don't think I can write ext \<a,b,rfl\>

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 17:19):

Did you try?

view this post on Zulip Yury G. Kudryashov (May 29 2020 at 17:19):

ext ⟨x⟩ works

view this post on Zulip Johan Commelin (May 29 2020 at 17:20):

Oooh, I never noticed!

view this post on Zulip Bryan Gin-ge Chen (May 29 2020 at 17:20):

Does the docstring / tactic doc need an update?


Last updated: May 14 2021 at 12:18 UTC