Zulip Chat Archive

Stream: general

Topic: How to introduce Implicit arguments in pattern matching?

Notification Bot (Dec 27 2022 at 14:47):

Erika Su has marked this topic as resolved.

Notification Bot (Dec 27 2022 at 14:47):

Erika Su has marked this topic as unresolved.

Notification Bot (Dec 27 2022 at 14:47):

Erika Su has marked this topic as resolved.

Notification Bot (Dec 27 2022 at 14:47):

Erika Su has marked this topic as unresolved.

Henrik Böving (Dec 27 2022 at 14:58):

If you know it is a palindrome you can always get the last element by returning the first element. The pattern matching you are trying here wont work because what you are doing is not a pattern match in the Lean sense.

Last updated: Dec 20 2023 at 11:08 UTC