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 28 at 2:17 | vote | accept | Greg Nisbet | ||
| Jun 29 at 17:27 | |||||
| Jun 27 at 4:37 | comment | added | Yannick Zakowski |
To do something similar to ssreflect in vanilla Ltac you can for instance go for: intros []; repeat match goal with | b : bool |- _ => destruct b end; reflexivity.
|
|
| Jun 27 at 4:17 | history | answered | djao | CC BY-SA 4.0 |