## 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. *) |