Zulip Chat Archive
Stream: general
Topic: rfunext
Johan Commelin (May 29 2020 at 13:58):
Do people want a rfunext tactic, that is to funext what rintro is to intro?
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
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
Johan Commelin (May 29 2020 at 14:00):
How about a tactic that uses machine learning to guess which tactics I want?
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.
Reid Barton (May 29 2020 at 14:03):
Do you mean ext?
Johan Commelin (May 29 2020 at 14:04):
rext?
Johan Commelin (May 29 2020 at 14:04):
I don't think I can write ext \<a,b,rfl\>
Yury G. Kudryashov (May 29 2020 at 17:19):
Did you try?
Yury G. Kudryashov (May 29 2020 at 17:19):
ext ⟨x⟩ works
Johan Commelin (May 29 2020 at 17:20):
Oooh, I never noticed!
Bryan Gin-ge Chen (May 29 2020 at 17:20):
Does the docstring / tactic doc need an update?
Last updated: Dec 20 2023 at 11:08 UTC