Mercurial > cpdt > repo

comparison 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
comparison
equal deleted inserted replaced
189:0198181d1b64 190:094bd1e353dd
32 rewrite (ext_eq _ _ _ H); trivial. 32 rewrite (ext_eq _ _ _ H); trivial.
33 Qed. 33 Qed.
34 34
35 Ltac ext_eq := (apply ext_eq || apply ext_eq_Set 35 Ltac ext_eq := (apply ext_eq || apply ext_eq_Set
36 || apply ext_eq_forall); intro. 36 || apply ext_eq_forall); intro.
37
38
39 Theorem eta : forall (A B : Type) (f : A -> B),
40 (fun x => f x) = f.
41 intros; ext_eq; trivial.
42 Qed.