Timeline for Is eta-equality provable in Coq?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 10, 2022 at 21:32 | comment | added | Couchy | @GuyCoder it should probably be a synonym | |
| Feb 10, 2022 at 11:55 | answer | added | Meven Lennon-Bertrand♦ | timeline score: 10 | |
| Feb 10, 2022 at 7:53 | comment | added | Trebor♦ | It should be noted that even if we have reduction rules related to eta-equality, we would usually do expansion instead of contraction, because it leads to better theoretic properties. | |
| Feb 10, 2022 at 7:11 | history | edited | Couchy | CC BY-SA 4.0 |
added 183 characters in body
|
| Feb 10, 2022 at 7:07 | vote | accept | Couchy | ||
| Feb 10, 2022 at 6:54 | answer | added | sarahzrf | timeline score: 19 | |
| Feb 10, 2022 at 6:39 | history | edited | Couchy | CC BY-SA 4.0 |
added 4 characters in body
|
| Feb 10, 2022 at 6:32 | history | asked | Couchy | CC BY-SA 4.0 |