## 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\>

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: May 14 2021 at 12:18 UTC