Mercurial > cpdt > repo
comparison src/Axioms.v @ 125:8a548a6c7074
Add ext_eq axiom and DepList notations
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 20 Oct 2008 10:44:20 -0400 |
| parents | |
| children | 7fd470d8a788 |
comparison
equal
deleted
inserted
replaced
| 124:57eaceb085f6 | 125:8a548a6c7074 |
|---|---|
| 1 (* Copyright (c) 2008, Adam Chlipala | |
| 2 * | |
| 3 * This work is licensed under a | |
| 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | |
| 5 * Unported License. | |
| 6 * The license text is available at: | |
| 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ | |
| 8 *) | |
| 9 | |
| 10 (* Additional axioms not in the Coq standard library *) | |
| 11 | |
| 12 Axiom ext_eq : forall (A : Type) (B : A -> Type) | |
| 13 (f g : forall x, B x), | |
| 14 (forall x, f x = g x) | |
| 15 -> f = g. | |
| 16 | |
| 17 Ltac ext_eq := apply ext_eq; intro. |