Zulip Chat Archive

Stream: general

Topic: rcases abuse

Patrick Massot (Jul 25 2018 at 15:45):

I think I set a new record for my uses of rcases with rcases r_in with ⟨t_α, ⟨r_α, r_α_in, h_α⟩, t_β, ⟨r_β, r_β_in, h_β⟩, h⟩,

Simon Hudon (Jul 25 2018 at 15:46):

Do you think you should be sent to Lean jail? I tend to prefer just a slap on the wrist but I'm open to hearing your arguments

Patrick Massot (Jul 25 2018 at 15:47):

Heh, it took me a while to figure out where to put bracket. This is an artistic performance.

Patrick Massot (Jul 25 2018 at 15:48):

Also, I blame product uniformities.

Last updated: Dec 20 2023 at 11:08 UTC