blob: f17fecc1e2b694ee458f9c2a4672861a7dbce12f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* The "?" of cons and eq should be inferred *)
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;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).
|
