Zulip Chat Archive

Stream: general

Topic: rcases?


view this post on Zulip Reid Barton (Sep 07 2018 at 10:43):

Is there a way to use rcases with ? to get hints, or just rintros?

view this post on Zulip Reid Barton (Sep 07 2018 at 11:00):

Wait, how do I use rintros? again? It's telling me "unexpected token".

view this post on Zulip Kevin Buzzard (Sep 07 2018 at 11:49):

rintros works for me. Is it in tactic.interactive? Looks like it. Note also meta def rintros := rintro ;-)

view this post on Zulip Kenny Lau (Sep 07 2018 at 12:45):

@Kevin Buzzard note the question mark in rintros?

view this post on Zulip Johan Commelin (Sep 07 2018 at 12:53):

@Kenny Lau You missed a chance to formulate that as a question.


Last updated: May 06 2021 at 22:13 UTC