From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- test-suite/success/evars.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 test-suite/success/evars.v (limited to 'test-suite/success/evars.v') diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v new file mode 100644 index 00000000..a7b6d6d8 --- /dev/null +++ b/test-suite/success/evars.v @@ -0,0 +1,23 @@ +(* The "?" of cons and eq should be inferred *) +Variable list:Set -> Set. +Variable cons:(T:Set) T -> (list T) -> (list T). +Check (n:(list nat)) (EX l| (EX x| (n = (cons ? x l)))). + +(* Examples provided by Eduardo Gimenez *) + +Definition c [A;Q:(nat*A->Prop)->Prop;P] := + (Q [p:nat*A]let (i,v) = p in (P i v)). + +(* What does this test ? *) +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). + +(* Checks that solvable ? in the lambda prefix of the definition are harmless*) +Parameter A1,A2,F,B,C : Set. +Parameter f : F -> A1 -> B. +Definition f1 [frm0,a1]: B := (f frm0 a1). + +(* Checks that solvable ? in the type part of the definition are harmless *) +Definition f2 : (frm0:?;a1:?)B := [frm0,a1](f frm0 a1). + -- cgit v1.2.3