-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathArgumentsScope.out
134 lines (111 loc) · 2.84 KB
/
ArgumentsScope.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
a : bool -> bool
a is not universe polymorphic
Arguments a _%bool_scope
Expands to: Variable a
b : bool -> bool
b is not universe polymorphic
Arguments b _%bool_scope
Expands to: Variable b
negb'' : bool -> bool
negb'' is not universe polymorphic
Arguments negb'' b%bool_scope
negb'' is transparent
Expands to: Constant ArgumentsScope.A.B.negb''
negb' : bool -> bool
negb' is not universe polymorphic
Arguments negb' b%bool_scope
negb' is transparent
Expands to: Constant ArgumentsScope.A.negb'
negb : bool -> bool
negb is not universe polymorphic
Arguments negb b%bool_scope
negb is transparent
Expands to: Constant Stdlib.Init.Datatypes.negb
a : bool -> bool
a is not universe polymorphic
Expands to: Variable a
b : bool -> bool
b is not universe polymorphic
Expands to: Variable b
negb : bool -> bool
negb is not universe polymorphic
Arguments negb b
negb is transparent
Expands to: Constant Stdlib.Init.Datatypes.negb
negb' : bool -> bool
negb' is not universe polymorphic
Arguments negb' b
negb' is transparent
Expands to: Constant ArgumentsScope.A.negb'
negb'' : bool -> bool
negb'' is not universe polymorphic
Arguments negb'' b
negb'' is transparent
Expands to: Constant ArgumentsScope.A.B.negb''
a : bool -> bool
a is not universe polymorphic
Expands to: Variable a
negb : bool -> bool
negb is not universe polymorphic
Arguments negb b
negb is transparent
Expands to: Constant Stdlib.Init.Datatypes.negb
negb' : bool -> bool
negb' is not universe polymorphic
Arguments negb' b
negb' is transparent
Expands to: Constant ArgumentsScope.negb'
negb'' : bool -> bool
negb'' is not universe polymorphic
Arguments negb'' b
negb'' is transparent
Expands to: Constant ArgumentsScope.negb''
f : bool -> bool
f is not universe polymorphic
Arguments f x%A_scope%B_scope
f is transparent
Expands to: Constant ArgumentsScope.f
f tt
: bool
f true
: bool
f : bool -> bool
f is not universe polymorphic
Arguments f x%B_scope%A_scope
f is transparent
Expands to: Constant ArgumentsScope.f
f tt
: bool
f false
: bool
g : bool -> bool
g is not universe polymorphic
Arguments g x%A_scope%B_scope
g is transparent
Expands to: Constant ArgumentsScope.g
g' : nat -> nat
g' is not universe polymorphic
Arguments g' x%B_scope%A_scope
g' is transparent
Expands to: Constant ArgumentsScope.g'
g'' : unit -> unit
g'' is not universe polymorphic
Arguments g'' x%B_scope
g'' is transparent
Expands to: Constant ArgumentsScope.g''
f : A -> B -> A
f is not universe polymorphic
Arguments f _%X _%Y
f is transparent
Expands to: Constant ArgumentsScope.SectionTest1.S.f
f : A -> B -> A
f is not universe polymorphic
f is transparent
Expands to: Constant ArgumentsScope.SectionTest1.f
N.f : A -> A
N.f is not universe polymorphic
Arguments N.f _%X
Expands to: Constant ArgumentsScope.SectionTest2.N.f
g : A -> A
g is not universe polymorphic
Expands to: Constant ArgumentsScope.SectionTest2.g