Timeline for Problem proving a binary add function
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 19, 2022 at 5:44 | history | rollback | Trebor♦ |
Rollback to Revision 7
|
|
| Apr 17, 2022 at 19:20 | history | edited | user1231 | CC BY-SA 4.0 |
deleted 694 characters in body
|
| Apr 16, 2022 at 19:20 | answer | added | Ms. Molly Stewart-Gallus | timeline score: 2 | |
| Apr 16, 2022 at 17:39 | vote | accept | CommunityBot | ||
| Apr 16, 2022 at 17:34 | vote | accept | CommunityBot | ||
| Apr 16, 2022 at 17:39 | |||||
| Apr 16, 2022 at 12:33 | history | edited | user1231 | CC BY-SA 4.0 |
added 597 characters in body
|
| Apr 15, 2022 at 18:20 | history | edited | user1231 | CC BY-SA 4.0 |
deleted 19 characters in body
|
| Apr 15, 2022 at 18:00 | history | edited | user1231 | CC BY-SA 4.0 |
added 114 characters in body
|
| Apr 15, 2022 at 16:15 | comment | added | Meven Lennon-Bertrand♦ |
If you want people to easily replay your proofs, you should give your whole context. For instance, here we lack the definition of value to be able to follow.
|
|
| Apr 15, 2022 at 15:55 | answer | added | Trebor♦ | timeline score: 3 | |
| Apr 15, 2022 at 15:28 | history | edited | user1231 | CC BY-SA 4.0 |
added 59 characters in body
|
| Apr 15, 2022 at 15:16 | comment | added | Trebor♦ |
Since the function badd matches on l2 and not l1, the rule of thumb is induction on l2: This "fits" the structure of the function, and is more likely to work. (Don't forget to generalize l1 before you make the induction.)
|
|
| Apr 15, 2022 at 15:11 | comment | added | Trebor♦ |
Have you proved that value (bsucc l) = 1 + value l ?
|
|
| Apr 15, 2022 at 15:10 | history | edited | Guy Coder | CC BY-SA 4.0 |
typo
|
| Apr 15, 2022 at 15:04 | history | edited | user1231 |
edited tags
|
|
| S Apr 15, 2022 at 15:02 | review | First questions | |||
| Apr 15, 2022 at 19:25 | |||||
| S Apr 15, 2022 at 15:02 | history | asked | user1231 | CC BY-SA 4.0 |