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
132
133
134
135
136
137
138
139
140
|
existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
existT is template universe polymorphic
Argument A is implicit
Argument scopes are [type_scope _ _ _]
Expands to: Constructor Coq.Init.Specif.existT
Inductive sigT (A : Type) (P : A -> Type) : Type :=
existT : forall x : A, P x -> {x : A & P x}
For sigT: Argument A is implicit
For existT: Argument A is implicit
For sigT: Argument scopes are [type_scope type_scope]
For existT: Argument scopes are [type_scope _ _ _]
existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
Argument A is implicit
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
For eq: Argument A is implicit and maximally inserted
For eq_refl, when applied to no arguments:
Arguments A, x are implicit and maximally inserted
For eq_refl, when applied to 1 argument:
Argument A 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
When applied to no arguments:
Arguments A, x are implicit and maximally inserted
When applied to 1 argument:
Argument A is implicit
Argument scopes are [type_scope _]
Expands to: Constructor Coq.Init.Logic.eq_refl
eq_refl : forall (A : Type) (x : A), x = x
When applied to no arguments:
Arguments A, x are implicit and maximally inserted
When applied to 1 argument:
Argument A is implicit
Nat.add =
fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end
: nat -> nat -> nat
Argument scopes are [nat_scope nat_scope]
Nat.add : nat -> nat -> nat
Argument scopes are [nat_scope nat_scope]
Nat.add is transparent
Expands to: Constant Coq.Init.Nat.add
Nat.add : nat -> nat -> nat
plus_n_O : forall n : nat, n = n + 0
Argument scope is [nat_scope]
plus_n_O is opaque
Expands to: Constant Coq.Init.Peano.plus_n_O
Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
For le_S: Argument m is implicit
For le_S: Argument n is implicit and maximally inserted
For le: Argument scopes are [nat_scope nat_scope]
For le_n: Argument scope is [nat_scope]
For le_S: Argument scopes are [nat_scope nat_scope _]
Inductive le (n : nat) : nat -> Prop :=
le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
For le_S: Argument m is implicit
For le_S: Argument n is implicit and maximally inserted
For le: Argument scopes are [nat_scope nat_scope]
For le_n: Argument scope is [nat_scope]
For le_S: Argument scopes are [nat_scope nat_scope _]
comparison : Set
Expands to: Inductive Coq.Init.Datatypes.comparison
Inductive comparison : Set :=
Eq : comparison | Lt : comparison | Gt : comparison
bar : foo
Expanded type for implicit arguments
bar : forall x : nat, x = 0
Argument x is implicit and maximally inserted
Expands to: Constant Top.bar
*** [ bar : foo ]
Expanded type for implicit arguments
bar : forall x : nat, x = 0
Argument x is implicit and maximally inserted
bar : foo
Expanded type for implicit arguments
bar : forall x : nat, x = 0
Argument x is implicit and maximally inserted
Expands to: Constant Top.bar
*** [ bar : foo ]
Expanded type for implicit arguments
bar : forall x : nat, x = 0
Argument x is implicit and maximally inserted
Module Coq.Init.Peano
Notation existS2 := existT2
Expands to: Notation Coq.Init.Specif.existS2
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
For eq: Argument A is implicit and maximally inserted
For eq_refl, when applied to no arguments:
Arguments A, x are implicit and maximally inserted
For eq_refl, when applied to 1 argument:
Argument A is implicit and maximally inserted
For eq: Argument scopes are [type_scope _ _]
For eq_refl: Argument scopes are [type_scope _]
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
For eq: Argument A is implicit and maximally inserted
For eq_refl, when applied to no arguments:
Arguments A, x are implicit and maximally inserted
For eq_refl, when applied to 1 argument:
Argument A is implicit and maximally inserted
For eq: Argument scopes are [type_scope _ _]
For eq_refl: Argument scopes are [type_scope _]
n:nat
Hypothesis of the goal context.
h:(n <> newdef n)
Hypothesis of the goal context.
g:(nat -> nat)
Constant (let in) of the goal context.
h:(n <> newdef n)
Hypothesis of the goal context.
|
