Mercurial > cpdt > repo
comparison src/GeneralRec.v @ 524:8f9f1e5b2fe3
Fix HTML formatting bug
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 02 Feb 2014 12:48:15 -0500 |
parents | 3b21f4395178 |
children | ed829eaa91b2 |
comparison
equal
deleted
inserted
replaced
523:4fa683368958 | 524:8f9f1e5b2fe3 |
---|---|
938 Theorem test_map : run (map (fun x => Return (S x)) (1 :: 2 :: 3 :: nil)) | 938 Theorem test_map : run (map (fun x => Return (S x)) (1 :: 2 :: 3 :: nil)) |
939 (2 :: 3 :: 4 :: nil). | 939 (2 :: 3 :: 4 :: nil). |
940 exists 1; reflexivity. | 940 exists 1; reflexivity. |
941 Qed. | 941 Qed. |
942 | 942 |
943 (** One further disadvantage of [comp] is that we cannot prove an inversion lemma for executions of [Bind] without appealing to an %\emph{axiom}%, a logical complication that we discuss at more length in Chapter 12. The other three techniques allow proof of all the important theorems within the normal logic of Coq. | 943 (** One further disadvantage of [comp] is that we cannot prove an inversion lemma for executions of [Bind] without appealing to an _axiom_, a logical complication that we discuss at more length in Chapter 12. The other three techniques allow proof of all the important theorems within the normal logic of Coq. |
944 | 944 |
945 Perhaps one theme of our comparison is that one must trade off between, on one hand, functional programming expressiveness and compatibility with normal Coq types and computation; and, on the other hand, the level of proof obligations one is willing to handle at function definition time. *) | 945 Perhaps one theme of our comparison is that one must trade off between, on one hand, functional programming expressiveness and compatibility with normal Coq types and computation; and, on the other hand, the level of proof obligations one is willing to handle at function definition time. *) |