-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathArguments.out
135 lines (120 loc) · 4.47 KB
/
Arguments.out
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
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub (n m)%nat_scope : simpl nomatch
The reduction tactics unfold Nat.sub but avoid exposing match constructs
Nat.sub is transparent
Expands to: Constant Stdlib.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub n%nat_scope / m%nat_scope : simpl nomatch
The reduction tactics unfold Nat.sub when applied to 1 argument
but avoid exposing match constructs
Nat.sub is transparent
Expands to: Constant Stdlib.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub !n%nat_scope / m%nat_scope : simpl nomatch
The reduction tactics unfold Nat.sub
when the 1st argument evaluates to a constructor and
when applied to 1 argument but avoid exposing match constructs
Nat.sub is transparent
Expands to: Constant Stdlib.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub (!n !m)%nat_scope /
The reduction tactics unfold Nat.sub when the 1st and
2nd arguments evaluate to a constructor and when applied to 2 arguments
Nat.sub is transparent
Expands to: Constant Stdlib.Init.Nat.sub
Nat.sub : nat -> nat -> nat
Nat.sub is not universe polymorphic
Arguments Nat.sub (!n !m)%nat_scope
The reduction tactics unfold Nat.sub when the 1st and
2nd arguments evaluate to a constructor
Nat.sub is transparent
Expands to: Constant Stdlib.Init.Nat.sub
pf :
forall {D1 C1 : Type},
(D1 -> C1) -> forall [D2 C2 : Type], (D2 -> C2) -> D1 * D2 -> C1 * C2
pf is not universe polymorphic
Arguments pf {D1}%foo_scope {C1}%type_scope f [D2 C2] g x : simpl never
The reduction tactics never unfold pf
pf is transparent
Expands to: Constant Arguments.pf
fcomp : forall {A B C : Type}, (B -> C) -> (A -> B) -> A -> C
fcomp is not universe polymorphic
Arguments fcomp {A B C}%type_scope f g x /
The reduction tactics unfold fcomp when applied to 6 arguments
fcomp is transparent
Expands to: Constant Arguments.fcomp
volatile : nat -> nat
volatile is not universe polymorphic
Arguments volatile / x%nat_scope
The reduction tactics always unfold volatile
volatile is transparent
Expands to: Constant Arguments.volatile
f : T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f x y n%nat_scope v m%nat_scope
f uses section variables T1 T2.
f is transparent
Expands to: Constant Arguments.S1.S2.f
f : T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f x y !n%nat_scope !v !m%nat_scope
f uses section variables T1 T2.
The reduction tactics unfold f when the 3rd, 4th and
5th arguments evaluate to a constructor
f is transparent
Expands to: Constant Arguments.S1.S2.f
f : forall [T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f [T2]%type_scope x y !n%nat_scope !v !m%nat_scope
f uses section variable T1.
The reduction tactics unfold f when the 4th, 5th and
6th arguments evaluate to a constructor
f is transparent
Expands to: Constant Arguments.S1.f
f : forall [T1 T2 : Type], T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f [T1 T2]%type_scope x y !n%nat_scope !v !m%nat_scope
The reduction tactics unfold f when the 5th, 6th and
7th arguments evaluate to a constructor
f is transparent
Expands to: Constant Arguments.f
= forall v : unit, f 0 0 5 v 3 = 2
: Prop
= 2 = 2
: Prop
f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
f is not universe polymorphic
Arguments f T1 T2 x y !n !v !m
The reduction tactics unfold f when the 5th, 6th and
7th arguments evaluate to a constructor
f is transparent
Expands to: Constant Arguments.f
forall w : r, w 3 true = tt
: Prop
File "./output/Arguments.v", line 52, characters 28-29:
The command has indeed failed with message:
Unknown interpretation for notation "$".
w 3 true = tt
: Prop
File "./output/Arguments.v", line 56, characters 0-28:
The command has indeed failed with message:
Extra arguments: _, _.
volatilematch : nat -> nat
volatilematch is not universe polymorphic
Arguments volatilematch / n%nat_scope : simpl nomatch
The reduction tactics always unfold volatilematch
but avoid exposing match constructs
volatilematch is transparent
Expands to: Constant Arguments.volatilematch
= fun n : nat => volatilematch n
: nat -> nat
*** [ f :
A ->
forall xxxxxxxxxxxxxx' xxxxxxxxxxxxxx'' : nat,
nat -> xxxxxxxxxxxxxx' + xxxxxxxxxxxxxx' + xxxxxxxxxxxxxx'' = 0 ]
Arguments f xxxxxxxxxxxxxx
(xxxxxxxxxxxxxx' xxxxxxxxxxxxxx'' xxxxxxxxxxxxxx''')%nat_scope