Timeline for Less ridiculous way to prove that an Ascii character compares equal with itself in Coq
Current License: CC BY-SA 4.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 29 at 17:27 | vote | accept | Greg Nisbet | ||
| Jun 29 at 6:57 | comment | added | Feryll | This is the best answer, both technically and perspectivally. One should prove facts about definitions using API-like lemmas about its direct subcomponents, i.e. at as high a level as possible. Theories built on intrinsic rather than extrinsic definitions. This makes it more readable and resilient to change. | |
| Jun 27 at 6:57 | history | answered | Li-yao Xia | CC BY-SA 4.0 |