blob: 23853890d8b2a35fc704fd0c961d2c36bac77515 (
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(* Testing the behavior of implicit arguments *)
(* Implicit on section variables *)
Set Implicit Arguments.
Unset Strict Implicit.
(* Example submitted by David Nowak *)
Section Spec.
Variable A : Set.
Variable op : forall A : Set, A -> A -> Set.
Infix "#" := op (at level 70).
Check (forall x : A, x # x).
(* Example submitted by Christine *)
Record stack : Type :=
{type : Set; elt : type; empty : type -> bool; proof : empty elt = true}.
Check
(forall (type : Set) (elt : type) (empty : type -> bool),
empty elt = true -> stack).
(* Nested sections and manual/automatic implicit arguments *)
Variable op' : forall A : Set, A -> A -> Set.
Variable op'' : forall A : Set, A -> A -> Set.
Section B.
Definition eq1 := fun (A:Type) (x y:A) => x=y.
Definition eq2 := fun (A:Type) (x y:A) => x=y.
Definition eq3 := fun (A:Type) (x y:A) => x=y.
Arguments op' : clear implicits.
Global Arguments op'' : clear implicits.
Arguments eq2 : clear implicits.
Global Arguments eq3 : clear implicits.
Check (op 0 0).
Check (op' nat 0 0).
Check (op'' nat 0 0).
Check (eq1 0 0).
Check (eq2 nat 0 0).
Check (eq3 nat 0 0).
End B.
Check (op 0 0).
Check (op' 0 0).
Check (op'' nat 0 0).
Check (eq1 0 0).
Check (eq2 0 0).
Check (eq3 nat 0 0).
End Spec.
Check (eq1 0 0).
Check (eq2 0 0).
Check (eq3 nat 0 0).
(* Example submitted by Frédéric (interesting in v8 syntax) *)
Parameter f : nat -> nat * nat.
Notation lhs := fst.
Check (fun x => fst (f x)).
Check (fun x => fst (f x)).
Notation rhs := snd.
Check (fun x => snd (f x)).
Check (fun x => @ rhs _ _ (f x)).
(* Implicit arguments in fixpoints and inductive declarations *)
Fixpoint g n := match n with O => true | S n => g n end.
Inductive P n : nat -> Prop := c : P n n.
(* Avoid evars in the computation of implicit arguments (cf r9827) *)
Require Import List.
Fixpoint plus n m {struct n} :=
match n with
| 0 => m
| S p => S (plus p m)
end.
(* Check multiple implicit arguments signatures *)
Arguments eq_refl {A x}, {A}.
Check eq_refl : 0 = 0.
(* Check that notations preserve implicit (since 8.3) *)
Parameter p : forall A, A -> forall n, n = 0 -> True.
Arguments p [A] _ [n].
Notation Q := (p 0).
Check Q eq_refl.
(* Check implicits with Context *)
Section C.
Context {A:Set}.
Definition h (a:A) := a.
End C.
Check h 0.
(* Check implicit arguments in arity of inductive types. The three
following examples used to fail before r13671 *)
Inductive I {A} (a:A) : forall {n:nat}, Prop :=
| C : I a (n:=0).
Inductive I2 (x:=0) : Prop :=
| C2 {p:nat} : p = 0 -> I2.
Check C2 eq_refl.
Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
| C3 : I3 a (n:=0).
(* Check global implicit declaration over ref not in section *)
Section D. Global Arguments eq [A] _ _. End D.
|
