Stream: new members

Topic: structure pattern matching

Olli (Aug 27 2018 at 17:08):

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 (Aug 27 2018 at 17:09):

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

Olli (Aug 27 2018 at 17:12):

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

Simon Hudon (Aug 27 2018 at 17:12):

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

Olli (Aug 27 2018 at 17:19):

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 (Aug 27 2018 at 17:31):

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 (Aug 27 2018 at 17:32):

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

Nice!

Olli (Aug 27 2018 at 17:36):

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

Last updated: May 08 2021 at 10:12 UTC