Zulip Chat Archive

Stream: new members

Topic: structure pattern matching


view this post on Zulip 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

view this post on Zulip Simon Hudon (Aug 27 2018 at 17:09):

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

view this post on Zulip Olli (Aug 27 2018 at 17:12):

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

view this post on Zulip Simon Hudon (Aug 27 2018 at 17:12):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Aug 27 2018 at 17:32):

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

view this post on Zulip Simon Hudon (Aug 27 2018 at 17:33):

Nice!

view this post on Zulip 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