diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-16 23:09:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-16 23:09:32 +0000 |
| commit | e3b51f8f1fb7249d3485ff7effa7df1a23c0282d (patch) | |
| tree | 9d728bb240655242fbd68ce1cc21fa8be5894788 /test-suite/success | |
| parent | cd279a01c50c9a5a236ff360709c569be08a5c80 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2196 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/evars.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 6d52ec4c6..13814d9d8 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -10,3 +10,10 @@ Variable list:Set -> Set. Variable cons:(T:Set) T -> (list T) -> (list T). Goal (n:(list nat)) (EX l| (EX x| (n = (cons ? x l)))). +(* Examples provided by Eduardo Gimenez *) + +Definition c [A,P] := [p:nat*A]let (i,v) = p in (P i v). + +Require PolyList. +Definition list_forall_bool [A:Set][p:A->bool][l:(list A)] : bool := + (fold_right ([a][r]if (p a) then r else false) true l).
\ No newline at end of file |