Zulip Chat Archive

Stream: new members

Topic: induction over nested sigma


????? (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.

Patrick Massot (Feb 13 2020 at 15:15):

rcases

Kevin Buzzard (Feb 13 2020 at 15:25):

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

????? (Feb 13 2020 at 17:24):

awesome, thanks!


Last updated: Dec 20 2023 at 11:08 UTC