Timeline for Questions about compilation errors in Coq
Current License: CC BY-SA 2.5
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 30, 2010 at 14:22 | comment | added | Per Vognsen | "The issue in the question is trying to find a particular monotonically decreasing measure function for the arguments of the Coq function being defined in order to prove that it terminates." I'm not sure I buy that. Any CS freshman who learns Floyd-Hoare logic for proving imperative programs correct routinely has to come up with much subtler termination measures for homework. So if that's really his question then it's disqualified on other grounds. Anyway, my opinion is that aspects of Coq's metatheory (calculus of inductive constructions, etc) are on topic but not mundane programming issues. | |
| Sep 30, 2010 at 14:06 | history | edited | Dave Clarke | CC BY-SA 2.5 |
added 192 characters in body
|
| Sep 30, 2010 at 13:51 | history | answered | Dave Clarke | CC BY-SA 2.5 |