Zulip Chat Archive

Stream: new members

Topic: induction over nested sigma


view this post on Zulip ????? (Feb 13 2020 at 15:14):

If I have a term t:Σx:A.Σy:B.Ct : \Sigma x:A. \Sigma y:B. C, is there a tactic equivalent to the pattern match match t with <x,y,p> := ... end? I want to extract the components all at once instead of repeating the induction tactic.

view this post on Zulip Patrick Massot (Feb 13 2020 at 15:15):

rcases

view this post on Zulip Kevin Buzzard (Feb 13 2020 at 15:25):

more precisely rcases t with ⟨x, y, p⟩

view this post on Zulip ????? (Feb 13 2020 at 17:24):

awesome, thanks!


Last updated: May 15 2021 at 23:13 UTC