Timeline for How can I prove this theorem with induction in Coq?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 18, 2022 at 21:59 | comment | added | Couchy |
FYI you can use repeat rewrite ... to repeat the rewrite until the goal no longer changes
|
|
| Apr 18, 2022 at 21:55 | comment | added | Nova Sczerin | wow thats a lot of rewrites! can ring be implemented instead somewhere? | |
| S Apr 18, 2022 at 18:56 | review | First answers | |||
| Apr 19, 2022 at 7:03 | |||||
| S Apr 18, 2022 at 18:56 | history | edited | Lessness Randomness | CC BY-SA 4.0 |
Gave partial solution, to show in some way why lia and similar tactics are necessary.
|
| S Apr 18, 2022 at 17:23 | review | First answers | |||
| Apr 18, 2022 at 18:52 | |||||
| S Apr 18, 2022 at 17:23 | history | answered | Lessness Randomness | CC BY-SA 4.0 |