Mercurial > cpdt > repo

annotate src/Axioms.v @ 125:8a548a6c7074

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
rev   line source
adamc@125 1 (* Copyright (c) 2008, Adam Chlipala
adamc@125 2 *
adamc@125 3 * This work is licensed under a
adamc@125 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@125 5 * Unported License.
adamc@125 6 * The license text is available at:
adamc@125 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@125 8 *)
adamc@125 9
adamc@125 10 (* Additional axioms not in the Coq standard library *)
adamc@125 11
adamc@125 12 Axiom ext_eq : forall (A : Type) (B : A -> Type)
adamc@125 13 (f g : forall x, B x),
adamc@125 14 (forall x, f x = g x)
adamc@125 15 -> f = g.
adamc@125 16
adamc@125 17 Ltac ext_eq := apply ext_eq; intro.