Mercurial > cpdt > repo

diff src/Axioms.v @ 190:094bd1e353dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Import predicative Impure example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 18 Nov 2008 12:44:46 -0500
parents 7fd470d8a788
children
line wrap: on
line diff
--- a/src/Axioms.v	Mon Nov 17 10:36:02 2008 -0500
+++ b/src/Axioms.v	Tue Nov 18 12:44:46 2008 -0500
@@ -34,3 +34,9 @@
 
 Ltac ext_eq := (apply ext_eq || apply ext_eq_Set
   || apply ext_eq_forall); intro.
+
+
+Theorem eta : forall (A B : Type) (f : A -> B),
+  (fun x => f x) = f.
+  intros; ext_eq; trivial.
+Qed.