Zulip Chat Archive
Stream: general
Topic: rcases?
Reid Barton (Sep 07 2018 at 10:43):
Is there a way to use rcases with ? to get hints, or just rintros?
Reid Barton (Sep 07 2018 at 11:00):
Wait, how do I use rintros? again? It's telling me "unexpected token".
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 ;-)
Kenny Lau (Sep 07 2018 at 12:45):
@Kevin Buzzard note the question mark in rintros?
Johan Commelin (Sep 07 2018 at 12:53):
@Kenny Lau You missed a chance to formulate that as a question.
Last updated: Dec 20 2023 at 11:08 UTC