Timeline for Prove simple theorems in Haskell in automated way
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 22, 2023 at 12:29 | vote | accept | Борат Сагдиев | ||
| Jun 22, 2023 at 12:29 | vote | accept | Борат Сагдиев | ||
| Jun 22, 2023 at 12:29 | |||||
| Jun 20, 2023 at 20:00 | comment | added | alias |
That's correct. Since sumToN already breaks the recursive cycle, sumToN_bad doesn't need to. It might be instructive to try both variants and look at the generated SMTLib output. Try inductNatWith z3{transcript = Just "debug.smt2"}and look at the differences in debug.smt2.
|
|
| Jun 20, 2023 at 17:48 | comment | added | Борат Сагдиев |
Notice we didn't call smtFunction. We could've; but we didn't need to. - am I understanding correctly that we didn't need to only because sumToN is already defined using smtFunction?
|
|
| Jun 10, 2023 at 13:28 | history | edited | alias | CC BY-SA 4.0 |
added 1 character in body
|
| Jun 10, 2023 at 6:45 | history | edited | alias | CC BY-SA 4.0 |
added 3 characters in body
|
| Jun 9, 2023 at 22:48 | history | edited | alias | CC BY-SA 4.0 |
edited body
|
| Jun 9, 2023 at 22:41 | history | edited | alias | CC BY-SA 4.0 |
edited body
|
| Jun 9, 2023 at 22:35 | history | edited | alias | CC BY-SA 4.0 |
added 2 characters in body
|
| Jun 9, 2023 at 22:30 | history | edited | alias | CC BY-SA 4.0 |
added 290 characters in body
|
| Jun 9, 2023 at 20:32 | history | answered | alias | CC BY-SA 4.0 |