Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 524:8f9f1e5b2fe3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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. *)