diff options
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 := |