Timeline for How to use a lemma that is defined in a Coq module?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 13 at 14:16 | vote | accept | The Circle | ||
| Apr 12 at 16:04 | answer | added | Hiroki Chen | timeline score: 2 | |
| Apr 12 at 16:04 | comment | added | Hiroki Chen | @AndrejBauer Sure :) | |
| Apr 12 at 12:52 | comment | added | Andrej Bauer | @HirokiChen: if you're so kind, please post your comment as an anwser, with a small working example demonstrating the solution. Thanks! | |
| Apr 12 at 12:51 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
edited title
|
| Apr 12 at 11:59 | history | edited | tinlyx | CC BY-SA 4.0 |
improved formatting
|
| Apr 7 at 17:35 | comment | added | The Circle |
Thank you, that solves my problem. I should have searched in Coq via Search or SearchPattern command instead
|
|
| Apr 7 at 17:12 | comment | added | Hiroki Chen |
Have you tried Require Import Arith. and then used that lemma by Nat.div_0_l?
|
|
| S Apr 7 at 16:19 | review | First questions | |||
| Apr 12 at 11:59 | |||||
| S Apr 7 at 16:19 | history | asked | The Circle | CC BY-SA 4.0 |