Reid Barton (Sep 07 2018 at 10:43):
Is there a way to use
? to get hints, or just
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
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