diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-06-24 13:54:23 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-06-24 13:54:23 +0000 |
| commit | 817b03d4d2bd752bf4bcfed273952334366431af (patch) | |
| tree | 0090b92cdbe580690e0fa3bb2845dbb0d0e08478 /contrib/dp/tests.v | |
| parent | 0ac9511b210cecee1d3e99deb509a0466a005ab7 (diff) | |
Dp: ajout d'abstraction aux applications de fonction non premier ordre
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7166 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/dp/tests.v')
| -rw-r--r-- | contrib/dp/tests.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v index 99a169d7e..d12203803 100644 --- a/contrib/dp/tests.v +++ b/contrib/dp/tests.v @@ -193,6 +193,16 @@ Qed. +(* abstractions *) + +Parameter poly_f : forall A:Set, A->A. + +Goal forall x:nat, poly_f nat x = poly_f nat x. +simplify. +Qed. + + + (* Anonymous mutually recursive functions : no equations are produced Definition mrf := |