Timeline for proof of termination for zip in Lean
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 30, 2023 at 22:33 | comment | added | Nate Glenn | Thank you! Adding parens makes it a pair instead of... I don't don't what it's called. A simultaneous match pattern? | |
| Aug 30, 2023 at 22:32 | vote | accept | Nate Glenn | ||
| Aug 30, 2023 at 14:58 | comment | added | Meven Lennon-Bertrand♦ | You are right, indeed, thanks. I edited the answer | |
| Aug 30, 2023 at 14:57 | history | edited | Meven Lennon-Bertrand♦ | CC BY-SA 4.0 |
Clarify statement that product is not an inductive type
|
| Aug 30, 2023 at 14:47 | comment | added | Jason Rute |
I’m not sure what you mean by “latter is not an inductive type”. Are you are saying that because product is a structure instead of an inductive type, that is the reason the termination checker fails. If so, I don’t think that is the reason. match works fine on structures as well as inductive types. I think it has more to do with the fact that you are matching on an inductive/structure type other than the inputs to the function.
|
|
| Aug 30, 2023 at 10:05 | history | answered | Meven Lennon-Bertrand♦ | CC BY-SA 4.0 |