structure pattern matching

Stream: new members

[Olli]

is it possible to pattern match structures? I saw on the PDF version of Theorem Proving in Lean (which I am guessing is now outdated based on other syntax differences) it is used, but the HTML version makes no mention of it, and none of my obvious guesses are working

[Simon Hudon]

Yes you can. Normally, the constructor is named my_struct.mk

[Olli]

ah yes that works, I was trying to use the ⦃ field, .. ⦄ syntax

[Simon Hudon]

Those are not the right brackets. You need ⟨ field1, ... ⟩

[Olli]

yeah the new book doesn't mention ⦃ ... ⦄, I think the old one did. I was trying to use it in the same manner as the field updates work, where I don't have to know the order of the fields, and I thought maybe it is possible to use { field, .. } with the two dots to match only a single field (while handling the other fields in other match arms

[Simon Hudon]

I see, I bit like in Haskell. I'm not aware of such a syntax in Lean but @Sebastian Ullrich or @Mario Carneiro might correct me.

[Sebastian Ullrich]

{ field := pat, .. } should absolutely work as a pattern

[Simon Hudon]

Nice!

[Olli]

thanks, I swear I tried that but I must have gotten something unrelated wrong :)