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
127
128
129
130
131
|
File "stdin", line 1, characters 0-36:
Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
[arguments-ignore-rename-nonimpl,vernacular]
The command has indeed failed with message:
Error:
To rename arguments the "rename" flag must be specified.
Argument A renamed to B.
File "stdin", line 2, characters 0-25:
Warning: Ignoring rename of A into T. Only implicit arguments can be renamed.
[arguments-ignore-rename-nonimpl,vernacular]
File "stdin", line 2, characters 0-25:
Warning: This command is just asserting the number and names of arguments of
identity. If this is what you want add ': assert' to silence the warning. If
you want to clear implicit arguments add ': clear implicits'. If you want to
clear notation scopes add ': clear scopes' [arguments-assert,vernacular]
File "stdin", line 4, characters 0-40:
Warning: Ignoring rename of x into y. Only implicit arguments can be renamed.
[arguments-ignore-rename-nonimpl,vernacular]
@eq_refl
: forall (B : Type) (y : B), y = y
eq_refl
: ?y = ?y
where
?y : [ |- nat]
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
For eq_refl: Arguments are renamed to B, y
For eq: Argument A is implicit and maximally inserted
For eq_refl, when applied to no arguments:
Arguments B, y are implicit and maximally inserted
For eq_refl, when applied to 1 argument:
Argument B is implicit
For eq: Argument scopes are [type_scope _ _]
For eq_refl: Argument scopes are [type_scope _]
eq_refl : forall (A : Type) (x : A), x = x
Arguments are renamed to B, y
When applied to no arguments:
Arguments B, y are implicit and maximally inserted
When applied to 1 argument:
Argument B is implicit
Argument scopes are [type_scope _]
Expands to: Constructor Coq.Init.Logic.eq_refl
Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x
For myrefl: Arguments are renamed to C, x, _
For myrefl: Argument C is implicit and maximally inserted
For myEq: Argument scopes are [type_scope _ _]
For myrefl: Argument scopes are [type_scope _ _]
myrefl : forall (B : Type) (x : A), B -> myEq B x x
Arguments are renamed to C, x, _
Argument C is implicit and maximally inserted
Argument scopes are [type_scope _ _]
Expands to: Constructor Top.Test1.myrefl
myplus =
fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S n' => S (myplus T t n' m)
end
: forall T : Type, T -> nat -> nat -> nat
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
myplus : forall T : Type, T -> nat -> nat -> nat
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
The reduction tactics unfold myplus when the 2nd and
3rd arguments evaluate to a constructor
myplus is transparent
Expands to: Constant Top.Test1.myplus
@myplus
: forall Z : Type, Z -> nat -> nat -> nat
Inductive myEq (A B : Type) (x : A) : A -> Prop :=
myrefl : B -> myEq A B x x
For myrefl: Arguments are renamed to A, C, x, _
For myrefl: Argument C is implicit and maximally inserted
For myEq: Argument scopes are [type_scope type_scope _ _]
For myrefl: Argument scopes are [type_scope type_scope _ _]
myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
Arguments are renamed to A, C, x, _
Argument C is implicit and maximally inserted
Argument scopes are [type_scope type_scope _ _]
Expands to: Constructor Top.myrefl
myrefl
: forall (A C : Type) (x : A), C -> myEq A C x x
myplus =
fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S n' => S (myplus T t n' m)
end
: forall T : Type, T -> nat -> nat -> nat
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
myplus : forall T : Type, T -> nat -> nat -> nat
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
The reduction tactics unfold myplus when the 2nd and
3rd arguments evaluate to a constructor
myplus is transparent
Expands to: Constant Top.myplus
@myplus
: forall Z : Type, Z -> nat -> nat -> nat
The command has indeed failed with message:
Error: All arguments lists must declare the same names.
The command has indeed failed with message:
Error: The following arguments are not declared: x.
The command has indeed failed with message:
Error: Arguments names must be distinct.
The command has indeed failed with message:
Error: Argument z cannot be declared implicit.
The command has indeed failed with message:
Error: Extra argument y.
File "stdin", line 53, characters 0-26:
Warning: Ignoring rename of x into s. Only implicit arguments can be renamed.
[arguments-ignore-rename-nonimpl,vernacular]
The command has indeed failed with message:
Error:
To rename arguments the "rename" flag must be specified.
Argument A renamed to R.
|
