| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (322 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (234 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (41 entries) |
Global Index
B
bounded_nat [library]bounded_even [library]
C
case_t_S [lemma, in BoundedNat.bounded_nat]D
double_half [lemma, in BoundedNat.even_half]double_half_in_nat_by_rect [lemma, in BoundedNat.bounded_even]
double_half_in_nat [definition, in BoundedNat.bounded_even]
D:100 [binder, in BoundedNat.bounded_even]
D:103 [binder, in BoundedNat.bounded_even]
D:146 [binder, in BoundedNat.bounded_even]
D:150 [binder, in BoundedNat.bounded_even]
D:156 [binder, in BoundedNat.bounded_even]
D:157 [binder, in BoundedNat.bounded_even]
D:76 [binder, in BoundedNat.bounded_even]
D:95 [binder, in BoundedNat.bounded_even]
D:99 [binder, in BoundedNat.bounded_even]
E
even [inductive, in BoundedNat.even_half]even [inductive, in BoundedNat.bounded_even]
evenTF [definition, in BoundedNat.even_half]
evenTF_mono [definition, in BoundedNat.even_half]
evenTF_back [definition, in BoundedNat.even_half]
evenTF_unique [definition, in BoundedNat.even_half]
even_rect [definition, in BoundedNat.even_half]
even_inv_π [definition, in BoundedNat.even_half]
even_unique_alt [lemma, in BoundedNat.even_half]
even_evenTF [definition, in BoundedNat.even_half]
even_unique [lemma, in BoundedNat.even_half]
even_plus_left [lemma, in BoundedNat.even_half]
even_inv [definition, in BoundedNat.even_half]
even_fold [definition, in BoundedNat.bounded_even]
even_rect [definition, in BoundedNat.bounded_even]
even_inv_π [definition, in BoundedNat.bounded_even]
even_lift2 [definition, in BoundedNat.bounded_even]
even_plus_left [lemma, in BoundedNat.bounded_even]
even_lift1 [definition, in BoundedNat.bounded_even]
even_2_inv [lemma, in BoundedNat.bounded_even]
even_inv [definition, in BoundedNat.bounded_even]
even_2 [constructor, in BoundedNat.bounded_even]
even_0 [constructor, in BoundedNat.bounded_even]
even_half [library]
Ev0 [constructor, in BoundedNat.even_half]
Ev2 [constructor, in BoundedNat.even_half]
e':105 [binder, in BoundedNat.even_half]
e':44 [binder, in BoundedNat.even_half]
e':47 [binder, in BoundedNat.even_half]
e':51 [binder, in BoundedNat.even_half]
e':55 [binder, in BoundedNat.even_half]
e':58 [binder, in BoundedNat.even_half]
e':62 [binder, in BoundedNat.even_half]
e':66 [binder, in BoundedNat.even_half]
e':70 [binder, in BoundedNat.even_half]
e':74 [binder, in BoundedNat.even_half]
e':78 [binder, in BoundedNat.even_half]
e':90 [binder, in BoundedNat.even_half]
e:101 [binder, in BoundedNat.even_half]
e:104 [binder, in BoundedNat.even_half]
e:107 [binder, in BoundedNat.even_half]
e:111 [binder, in BoundedNat.even_half]
e:113 [binder, in BoundedNat.bounded_even]
e:117 [binder, in BoundedNat.even_half]
e:117 [binder, in BoundedNat.bounded_even]
e:12 [binder, in BoundedNat.even_half]
e:120 [binder, in BoundedNat.even_half]
e:120 [binder, in BoundedNat.bounded_even]
e:122 [binder, in BoundedNat.even_half]
e:124 [binder, in BoundedNat.bounded_even]
e:125 [binder, in BoundedNat.even_half]
e:125 [binder, in BoundedNat.bounded_even]
e:126 [binder, in BoundedNat.even_half]
e:127 [binder, in BoundedNat.even_half]
e:128 [binder, in BoundedNat.even_half]
e:128 [binder, in BoundedNat.bounded_even]
e:129 [binder, in BoundedNat.bounded_even]
e:130 [binder, in BoundedNat.even_half]
e:130 [binder, in BoundedNat.bounded_even]
e:133 [binder, in BoundedNat.even_half]
e:133 [binder, in BoundedNat.bounded_even]
e:134 [binder, in BoundedNat.even_half]
e:135 [binder, in BoundedNat.even_half]
e:136 [binder, in BoundedNat.even_half]
e:137 [binder, in BoundedNat.bounded_even]
e:138 [binder, in BoundedNat.bounded_even]
e:14 [binder, in BoundedNat.even_half]
e:141 [binder, in BoundedNat.bounded_even]
e:142 [binder, in BoundedNat.bounded_even]
e:143 [binder, in BoundedNat.bounded_even]
e:160 [binder, in BoundedNat.bounded_even]
e:163 [binder, in BoundedNat.bounded_even]
e:17 [binder, in BoundedNat.bounded_even]
e:19 [binder, in BoundedNat.even_half]
e:20 [binder, in BoundedNat.bounded_even]
e:29 [binder, in BoundedNat.even_half]
e:32 [binder, in BoundedNat.even_half]
e:33 [binder, in BoundedNat.even_half]
e:35 [binder, in BoundedNat.even_half]
e:37 [binder, in BoundedNat.even_half]
e:40 [binder, in BoundedNat.even_half]
e:43 [binder, in BoundedNat.even_half]
e:46 [binder, in BoundedNat.even_half]
e:50 [binder, in BoundedNat.even_half]
e:54 [binder, in BoundedNat.even_half]
e:57 [binder, in BoundedNat.even_half]
e:61 [binder, in BoundedNat.even_half]
e:65 [binder, in BoundedNat.even_half]
e:69 [binder, in BoundedNat.even_half]
e:73 [binder, in BoundedNat.even_half]
e:77 [binder, in BoundedNat.even_half]
e:84 [binder, in BoundedNat.even_half]
e:84 [binder, in BoundedNat.bounded_even]
e:89 [binder, in BoundedNat.even_half]
e:89 [binder, in BoundedNat.bounded_even]
e:92 [binder, in BoundedNat.bounded_even]
e:97 [binder, in BoundedNat.even_half]
e:99 [binder, in BoundedNat.even_half]
F
F [definition, in BoundedNat.looping_absurd]fa:26 [binder, in BoundedNat.even_half]
fa:54 [binder, in BoundedNat.bounded_even]
fa:58 [binder, in BoundedNat.bounded_even]
fa:62 [binder, in BoundedNat.bounded_even]
fa:72 [binder, in BoundedNat.bounded_even]
fa:73 [binder, in BoundedNat.bounded_even]
fa:80 [binder, in BoundedNat.bounded_even]
Fexc [definition, in BoundedNat.looping_absurd]
Floop [definition, in BoundedNat.looping_absurd]
Floop_F [definition, in BoundedNat.looping_absurd]
Floop_T [definition, in BoundedNat.looping_absurd]
Floop_P [definition, in BoundedNat.looping_absurd]
FO [constructor, in BoundedNat.bounded_nat]
forget [definition, in BoundedNat.bounded_nat]
Fplus [definition, in BoundedNat.bounded_nat]
fpred2 [definition, in BoundedNat.bounded_even]
FS [constructor, in BoundedNat.bounded_nat]
f:12 [binder, in BoundedNat.looping_absurd]
f:17 [binder, in BoundedNat.looping_absurd]
f:21 [binder, in BoundedNat.looping_absurd]
f:8 [binder, in BoundedNat.looping_absurd]
G
G:25 [binder, in BoundedNat.even_half]G:65 [binder, in BoundedNat.bounded_even]
G:68 [binder, in BoundedNat.bounded_even]
G:71 [binder, in BoundedNat.bounded_even]
G:79 [binder, in BoundedNat.bounded_even]
H
half [definition, in BoundedNat.even_half]half_pcst [lemma, in BoundedNat.even_half]
half_in_t_by_fold [definition, in BoundedNat.bounded_even]
half_in_t [definition, in BoundedNat.bounded_even]
half_in_nat [definition, in BoundedNat.bounded_even]
ha:164 [binder, in BoundedNat.bounded_even]
h:104 [binder, in BoundedNat.bounded_even]
h:147 [binder, in BoundedNat.bounded_even]
I
iFF_iSS [definition, in BoundedNat.bounded_even]iFF_iSS_inter [lemma, in BoundedNat.bounded_even]
is_Ev2_π_intro [constructor, in BoundedNat.even_half]
is_Ev2_π [inductive, in BoundedNat.even_half]
is_Ev2_intro [constructor, in BoundedNat.even_half]
is_Ev2 [inductive, in BoundedNat.even_half]
is_Ev0_intro [constructor, in BoundedNat.even_half]
is_Ev0 [inductive, in BoundedNat.even_half]
is_even_2_π_intro [constructor, in BoundedNat.bounded_even]
is_even_2_π [inductive, in BoundedNat.bounded_even]
is_FS_FS [definition, in BoundedNat.bounded_even]
is_S_S [definition, in BoundedNat.bounded_even]
is_even_2_intro [constructor, in BoundedNat.bounded_even]
is_even_2 [inductive, in BoundedNat.bounded_even]
is_even_0_intro [constructor, in BoundedNat.bounded_even]
is_even_0 [inductive, in BoundedNat.bounded_even]
i:102 [binder, in BoundedNat.bounded_even]
i:107 [binder, in BoundedNat.bounded_even]
i:112 [binder, in BoundedNat.bounded_even]
i:116 [binder, in BoundedNat.bounded_even]
i:119 [binder, in BoundedNat.bounded_even]
i:132 [binder, in BoundedNat.bounded_even]
i:14 [binder, in BoundedNat.bounded_nat]
i:14 [binder, in BoundedNat.bounded_even]
i:145 [binder, in BoundedNat.bounded_even]
i:149 [binder, in BoundedNat.bounded_even]
i:159 [binder, in BoundedNat.bounded_even]
i:16 [binder, in BoundedNat.bounded_nat]
i:162 [binder, in BoundedNat.bounded_even]
i:19 [binder, in BoundedNat.bounded_even]
i:21 [binder, in BoundedNat.bounded_nat]
i:22 [binder, in BoundedNat.bounded_nat]
i:24 [binder, in BoundedNat.bounded_even]
i:25 [binder, in BoundedNat.bounded_nat]
i:27 [binder, in BoundedNat.bounded_even]
i:28 [binder, in BoundedNat.bounded_nat]
i:31 [binder, in BoundedNat.bounded_even]
i:34 [binder, in BoundedNat.bounded_nat]
i:34 [binder, in BoundedNat.bounded_even]
i:40 [binder, in BoundedNat.bounded_even]
i:46 [binder, in BoundedNat.bounded_even]
i:49 [binder, in BoundedNat.bounded_even]
i:51 [binder, in BoundedNat.bounded_even]
i:6 [binder, in BoundedNat.bounded_nat]
i:6 [binder, in BoundedNat.bounded_even]
i:75 [binder, in BoundedNat.bounded_even]
i:83 [binder, in BoundedNat.bounded_even]
i:88 [binder, in BoundedNat.bounded_even]
i:94 [binder, in BoundedNat.bounded_even]
J
j:32 [binder, in BoundedNat.bounded_even]j:35 [binder, in BoundedNat.bounded_nat]
j:64 [binder, in BoundedNat.bounded_even]
L
lift1 [definition, in BoundedNat.bounded_nat]lift2 [definition, in BoundedNat.bounded_even]
loop [definition, in BoundedNat.looping_absurd]
looping_absurd [library]
M
m:17 [binder, in BoundedNat.even_half]m:24 [binder, in BoundedNat.bounded_nat]
m:25 [binder, in BoundedNat.bounded_even]
m:26 [binder, in BoundedNat.bounded_nat]
m:30 [binder, in BoundedNat.bounded_even]
m:33 [binder, in BoundedNat.bounded_nat]
m:35 [binder, in BoundedNat.bounded_even]
m:41 [binder, in BoundedNat.bounded_even]
m:63 [binder, in BoundedNat.bounded_even]
N
no_Ev1 [inductive, in BoundedNat.even_half]no_even1 [inductive, in BoundedNat.bounded_even]
n:1 [binder, in BoundedNat.even_half]
n:1 [binder, in BoundedNat.bounded_even]
n:10 [binder, in BoundedNat.bounded_even]
n:100 [binder, in BoundedNat.even_half]
n:101 [binder, in BoundedNat.bounded_even]
n:103 [binder, in BoundedNat.even_half]
n:106 [binder, in BoundedNat.even_half]
n:106 [binder, in BoundedNat.bounded_even]
n:109 [binder, in BoundedNat.bounded_even]
n:11 [binder, in BoundedNat.bounded_nat]
n:110 [binder, in BoundedNat.even_half]
n:111 [binder, in BoundedNat.bounded_even]
n:113 [binder, in BoundedNat.even_half]
n:115 [binder, in BoundedNat.bounded_even]
n:116 [binder, in BoundedNat.even_half]
n:118 [binder, in BoundedNat.bounded_even]
n:119 [binder, in BoundedNat.even_half]
n:121 [binder, in BoundedNat.even_half]
n:129 [binder, in BoundedNat.even_half]
n:13 [binder, in BoundedNat.even_half]
n:13 [binder, in BoundedNat.bounded_even]
n:131 [binder, in BoundedNat.bounded_even]
n:144 [binder, in BoundedNat.bounded_even]
n:148 [binder, in BoundedNat.bounded_even]
n:15 [binder, in BoundedNat.bounded_nat]
n:158 [binder, in BoundedNat.bounded_even]
n:16 [binder, in BoundedNat.even_half]
n:161 [binder, in BoundedNat.bounded_even]
n:165 [binder, in BoundedNat.bounded_even]
n:18 [binder, in BoundedNat.bounded_nat]
n:18 [binder, in BoundedNat.even_half]
n:18 [binder, in BoundedNat.bounded_even]
n:20 [binder, in BoundedNat.bounded_nat]
n:23 [binder, in BoundedNat.bounded_nat]
n:23 [binder, in BoundedNat.even_half]
n:23 [binder, in BoundedNat.bounded_even]
n:26 [binder, in BoundedNat.bounded_even]
n:27 [binder, in BoundedNat.bounded_nat]
n:28 [binder, in BoundedNat.even_half]
n:29 [binder, in BoundedNat.bounded_even]
n:3 [binder, in BoundedNat.bounded_nat]
n:32 [binder, in BoundedNat.bounded_nat]
n:33 [binder, in BoundedNat.bounded_even]
n:34 [binder, in BoundedNat.even_half]
n:36 [binder, in BoundedNat.even_half]
n:39 [binder, in BoundedNat.even_half]
n:39 [binder, in BoundedNat.bounded_even]
n:4 [binder, in BoundedNat.bounded_nat]
n:4 [binder, in BoundedNat.even_half]
n:4 [binder, in BoundedNat.bounded_even]
n:42 [binder, in BoundedNat.even_half]
n:43 [binder, in BoundedNat.bounded_even]
n:45 [binder, in BoundedNat.even_half]
n:45 [binder, in BoundedNat.bounded_even]
n:48 [binder, in BoundedNat.bounded_even]
n:49 [binder, in BoundedNat.even_half]
n:5 [binder, in BoundedNat.bounded_nat]
n:5 [binder, in BoundedNat.bounded_even]
n:50 [binder, in BoundedNat.bounded_even]
n:53 [binder, in BoundedNat.even_half]
n:56 [binder, in BoundedNat.even_half]
n:60 [binder, in BoundedNat.even_half]
n:60 [binder, in BoundedNat.bounded_even]
n:64 [binder, in BoundedNat.even_half]
n:68 [binder, in BoundedNat.even_half]
n:7 [binder, in BoundedNat.bounded_even]
n:72 [binder, in BoundedNat.even_half]
n:74 [binder, in BoundedNat.bounded_even]
n:76 [binder, in BoundedNat.even_half]
n:80 [binder, in BoundedNat.even_half]
n:82 [binder, in BoundedNat.bounded_even]
n:83 [binder, in BoundedNat.even_half]
n:87 [binder, in BoundedNat.bounded_even]
n:88 [binder, in BoundedNat.even_half]
n:9 [binder, in BoundedNat.even_half]
n:93 [binder, in BoundedNat.bounded_even]
n:94 [binder, in BoundedNat.even_half]
P
P [definition, in BoundedNat.looping_absurd]pr2 [definition, in BoundedNat.bounded_even]
P0:110 [binder, in BoundedNat.bounded_even]
P0:115 [binder, in BoundedNat.even_half]
P2:114 [binder, in BoundedNat.bounded_even]
P2:118 [binder, in BoundedNat.even_half]
P:108 [binder, in BoundedNat.bounded_even]
P:114 [binder, in BoundedNat.even_half]
S
sec_example.P [variable, in BoundedNat.bounded_nat]sec_example [section, in BoundedNat.bounded_nat]
sec_absurd.p [variable, in BoundedNat.looping_absurd]
sec_absurd.f [variable, in BoundedNat.looping_absurd]
sec_absurd.X [variable, in BoundedNat.looping_absurd]
sec_absurd [section, in BoundedNat.looping_absurd]
shape_S_FS [constructor, in BoundedNat.bounded_nat]
shape_S_F0 [constructor, in BoundedNat.bounded_nat]
shape_S [inductive, in BoundedNat.bounded_nat]
shape_O [inductive, in BoundedNat.bounded_nat]
T
t [inductive, in BoundedNat.bounded_nat]T [definition, in BoundedNat.looping_absurd]
t_n_Sm [definition, in BoundedNat.bounded_nat]
t_inv [definition, in BoundedNat.bounded_nat]
t:16 [binder, in BoundedNat.looping_absurd]
X
X:11 [binder, in BoundedNat.looping_absurd]X:15 [binder, in BoundedNat.looping_absurd]
X:20 [binder, in BoundedNat.looping_absurd]
x:3 [binder, in BoundedNat.looping_absurd]
X:7 [binder, in BoundedNat.looping_absurd]
other
πeven [definition, in BoundedNat.even_half]πeven [definition, in BoundedNat.bounded_even]
Binder Index
D
D:100 [in BoundedNat.bounded_even]D:103 [in BoundedNat.bounded_even]
D:146 [in BoundedNat.bounded_even]
D:150 [in BoundedNat.bounded_even]
D:156 [in BoundedNat.bounded_even]
D:157 [in BoundedNat.bounded_even]
D:76 [in BoundedNat.bounded_even]
D:95 [in BoundedNat.bounded_even]
D:99 [in BoundedNat.bounded_even]
E
e':105 [in BoundedNat.even_half]e':44 [in BoundedNat.even_half]
e':47 [in BoundedNat.even_half]
e':51 [in BoundedNat.even_half]
e':55 [in BoundedNat.even_half]
e':58 [in BoundedNat.even_half]
e':62 [in BoundedNat.even_half]
e':66 [in BoundedNat.even_half]
e':70 [in BoundedNat.even_half]
e':74 [in BoundedNat.even_half]
e':78 [in BoundedNat.even_half]
e':90 [in BoundedNat.even_half]
e:101 [in BoundedNat.even_half]
e:104 [in BoundedNat.even_half]
e:107 [in BoundedNat.even_half]
e:111 [in BoundedNat.even_half]
e:113 [in BoundedNat.bounded_even]
e:117 [in BoundedNat.even_half]
e:117 [in BoundedNat.bounded_even]
e:12 [in BoundedNat.even_half]
e:120 [in BoundedNat.even_half]
e:120 [in BoundedNat.bounded_even]
e:122 [in BoundedNat.even_half]
e:124 [in BoundedNat.bounded_even]
e:125 [in BoundedNat.even_half]
e:125 [in BoundedNat.bounded_even]
e:126 [in BoundedNat.even_half]
e:127 [in BoundedNat.even_half]
e:128 [in BoundedNat.even_half]
e:128 [in BoundedNat.bounded_even]
e:129 [in BoundedNat.bounded_even]
e:130 [in BoundedNat.even_half]
e:130 [in BoundedNat.bounded_even]
e:133 [in BoundedNat.even_half]
e:133 [in BoundedNat.bounded_even]
e:134 [in BoundedNat.even_half]
e:135 [in BoundedNat.even_half]
e:136 [in BoundedNat.even_half]
e:137 [in BoundedNat.bounded_even]
e:138 [in BoundedNat.bounded_even]
e:14 [in BoundedNat.even_half]
e:141 [in BoundedNat.bounded_even]
e:142 [in BoundedNat.bounded_even]
e:143 [in BoundedNat.bounded_even]
e:160 [in BoundedNat.bounded_even]
e:163 [in BoundedNat.bounded_even]
e:17 [in BoundedNat.bounded_even]
e:19 [in BoundedNat.even_half]
e:20 [in BoundedNat.bounded_even]
e:29 [in BoundedNat.even_half]
e:32 [in BoundedNat.even_half]
e:33 [in BoundedNat.even_half]
e:35 [in BoundedNat.even_half]
e:37 [in BoundedNat.even_half]
e:40 [in BoundedNat.even_half]
e:43 [in BoundedNat.even_half]
e:46 [in BoundedNat.even_half]
e:50 [in BoundedNat.even_half]
e:54 [in BoundedNat.even_half]
e:57 [in BoundedNat.even_half]
e:61 [in BoundedNat.even_half]
e:65 [in BoundedNat.even_half]
e:69 [in BoundedNat.even_half]
e:73 [in BoundedNat.even_half]
e:77 [in BoundedNat.even_half]
e:84 [in BoundedNat.even_half]
e:84 [in BoundedNat.bounded_even]
e:89 [in BoundedNat.even_half]
e:89 [in BoundedNat.bounded_even]
e:92 [in BoundedNat.bounded_even]
e:97 [in BoundedNat.even_half]
e:99 [in BoundedNat.even_half]
F
fa:26 [in BoundedNat.even_half]fa:54 [in BoundedNat.bounded_even]
fa:58 [in BoundedNat.bounded_even]
fa:62 [in BoundedNat.bounded_even]
fa:72 [in BoundedNat.bounded_even]
fa:73 [in BoundedNat.bounded_even]
fa:80 [in BoundedNat.bounded_even]
f:12 [in BoundedNat.looping_absurd]
f:17 [in BoundedNat.looping_absurd]
f:21 [in BoundedNat.looping_absurd]
f:8 [in BoundedNat.looping_absurd]
G
G:25 [in BoundedNat.even_half]G:65 [in BoundedNat.bounded_even]
G:68 [in BoundedNat.bounded_even]
G:71 [in BoundedNat.bounded_even]
G:79 [in BoundedNat.bounded_even]
H
ha:164 [in BoundedNat.bounded_even]h:104 [in BoundedNat.bounded_even]
h:147 [in BoundedNat.bounded_even]
I
i:102 [in BoundedNat.bounded_even]i:107 [in BoundedNat.bounded_even]
i:112 [in BoundedNat.bounded_even]
i:116 [in BoundedNat.bounded_even]
i:119 [in BoundedNat.bounded_even]
i:132 [in BoundedNat.bounded_even]
i:14 [in BoundedNat.bounded_nat]
i:14 [in BoundedNat.bounded_even]
i:145 [in BoundedNat.bounded_even]
i:149 [in BoundedNat.bounded_even]
i:159 [in BoundedNat.bounded_even]
i:16 [in BoundedNat.bounded_nat]
i:162 [in BoundedNat.bounded_even]
i:19 [in BoundedNat.bounded_even]
i:21 [in BoundedNat.bounded_nat]
i:22 [in BoundedNat.bounded_nat]
i:24 [in BoundedNat.bounded_even]
i:25 [in BoundedNat.bounded_nat]
i:27 [in BoundedNat.bounded_even]
i:28 [in BoundedNat.bounded_nat]
i:31 [in BoundedNat.bounded_even]
i:34 [in BoundedNat.bounded_nat]
i:34 [in BoundedNat.bounded_even]
i:40 [in BoundedNat.bounded_even]
i:46 [in BoundedNat.bounded_even]
i:49 [in BoundedNat.bounded_even]
i:51 [in BoundedNat.bounded_even]
i:6 [in BoundedNat.bounded_nat]
i:6 [in BoundedNat.bounded_even]
i:75 [in BoundedNat.bounded_even]
i:83 [in BoundedNat.bounded_even]
i:88 [in BoundedNat.bounded_even]
i:94 [in BoundedNat.bounded_even]
J
j:32 [in BoundedNat.bounded_even]j:35 [in BoundedNat.bounded_nat]
j:64 [in BoundedNat.bounded_even]
M
m:17 [in BoundedNat.even_half]m:24 [in BoundedNat.bounded_nat]
m:25 [in BoundedNat.bounded_even]
m:26 [in BoundedNat.bounded_nat]
m:30 [in BoundedNat.bounded_even]
m:33 [in BoundedNat.bounded_nat]
m:35 [in BoundedNat.bounded_even]
m:41 [in BoundedNat.bounded_even]
m:63 [in BoundedNat.bounded_even]
N
n:1 [in BoundedNat.even_half]n:1 [in BoundedNat.bounded_even]
n:10 [in BoundedNat.bounded_even]
n:100 [in BoundedNat.even_half]
n:101 [in BoundedNat.bounded_even]
n:103 [in BoundedNat.even_half]
n:106 [in BoundedNat.even_half]
n:106 [in BoundedNat.bounded_even]
n:109 [in BoundedNat.bounded_even]
n:11 [in BoundedNat.bounded_nat]
n:110 [in BoundedNat.even_half]
n:111 [in BoundedNat.bounded_even]
n:113 [in BoundedNat.even_half]
n:115 [in BoundedNat.bounded_even]
n:116 [in BoundedNat.even_half]
n:118 [in BoundedNat.bounded_even]
n:119 [in BoundedNat.even_half]
n:121 [in BoundedNat.even_half]
n:129 [in BoundedNat.even_half]
n:13 [in BoundedNat.even_half]
n:13 [in BoundedNat.bounded_even]
n:131 [in BoundedNat.bounded_even]
n:144 [in BoundedNat.bounded_even]
n:148 [in BoundedNat.bounded_even]
n:15 [in BoundedNat.bounded_nat]
n:158 [in BoundedNat.bounded_even]
n:16 [in BoundedNat.even_half]
n:161 [in BoundedNat.bounded_even]
n:165 [in BoundedNat.bounded_even]
n:18 [in BoundedNat.bounded_nat]
n:18 [in BoundedNat.even_half]
n:18 [in BoundedNat.bounded_even]
n:20 [in BoundedNat.bounded_nat]
n:23 [in BoundedNat.bounded_nat]
n:23 [in BoundedNat.even_half]
n:23 [in BoundedNat.bounded_even]
n:26 [in BoundedNat.bounded_even]
n:27 [in BoundedNat.bounded_nat]
n:28 [in BoundedNat.even_half]
n:29 [in BoundedNat.bounded_even]
n:3 [in BoundedNat.bounded_nat]
n:32 [in BoundedNat.bounded_nat]
n:33 [in BoundedNat.bounded_even]
n:34 [in BoundedNat.even_half]
n:36 [in BoundedNat.even_half]
n:39 [in BoundedNat.even_half]
n:39 [in BoundedNat.bounded_even]
n:4 [in BoundedNat.bounded_nat]
n:4 [in BoundedNat.even_half]
n:4 [in BoundedNat.bounded_even]
n:42 [in BoundedNat.even_half]
n:43 [in BoundedNat.bounded_even]
n:45 [in BoundedNat.even_half]
n:45 [in BoundedNat.bounded_even]
n:48 [in BoundedNat.bounded_even]
n:49 [in BoundedNat.even_half]
n:5 [in BoundedNat.bounded_nat]
n:5 [in BoundedNat.bounded_even]
n:50 [in BoundedNat.bounded_even]
n:53 [in BoundedNat.even_half]
n:56 [in BoundedNat.even_half]
n:60 [in BoundedNat.even_half]
n:60 [in BoundedNat.bounded_even]
n:64 [in BoundedNat.even_half]
n:68 [in BoundedNat.even_half]
n:7 [in BoundedNat.bounded_even]
n:72 [in BoundedNat.even_half]
n:74 [in BoundedNat.bounded_even]
n:76 [in BoundedNat.even_half]
n:80 [in BoundedNat.even_half]
n:82 [in BoundedNat.bounded_even]
n:83 [in BoundedNat.even_half]
n:87 [in BoundedNat.bounded_even]
n:88 [in BoundedNat.even_half]
n:9 [in BoundedNat.even_half]
n:93 [in BoundedNat.bounded_even]
n:94 [in BoundedNat.even_half]
P
P0:110 [in BoundedNat.bounded_even]P0:115 [in BoundedNat.even_half]
P2:114 [in BoundedNat.bounded_even]
P2:118 [in BoundedNat.even_half]
P:108 [in BoundedNat.bounded_even]
P:114 [in BoundedNat.even_half]
T
t:16 [in BoundedNat.looping_absurd]X
X:11 [in BoundedNat.looping_absurd]X:15 [in BoundedNat.looping_absurd]
X:20 [in BoundedNat.looping_absurd]
x:3 [in BoundedNat.looping_absurd]
X:7 [in BoundedNat.looping_absurd]
Variable Index
S
sec_example.P [in BoundedNat.bounded_nat]sec_absurd.p [in BoundedNat.looping_absurd]
sec_absurd.f [in BoundedNat.looping_absurd]
sec_absurd.X [in BoundedNat.looping_absurd]
Library Index
B
bounded_natbounded_even
E
even_halfL
looping_absurdLemma Index
C
case_t_S [in BoundedNat.bounded_nat]D
double_half [in BoundedNat.even_half]double_half_in_nat_by_rect [in BoundedNat.bounded_even]
E
even_unique_alt [in BoundedNat.even_half]even_unique [in BoundedNat.even_half]
even_plus_left [in BoundedNat.even_half]
even_plus_left [in BoundedNat.bounded_even]
even_2_inv [in BoundedNat.bounded_even]
H
half_pcst [in BoundedNat.even_half]I
iFF_iSS_inter [in BoundedNat.bounded_even]Constructor Index
E
even_2 [in BoundedNat.bounded_even]even_0 [in BoundedNat.bounded_even]
Ev0 [in BoundedNat.even_half]
Ev2 [in BoundedNat.even_half]
F
FO [in BoundedNat.bounded_nat]FS [in BoundedNat.bounded_nat]
I
is_Ev2_π_intro [in BoundedNat.even_half]is_Ev2_intro [in BoundedNat.even_half]
is_Ev0_intro [in BoundedNat.even_half]
is_even_2_π_intro [in BoundedNat.bounded_even]
is_even_2_intro [in BoundedNat.bounded_even]
is_even_0_intro [in BoundedNat.bounded_even]
S
shape_S_FS [in BoundedNat.bounded_nat]shape_S_F0 [in BoundedNat.bounded_nat]
Inductive Index
E
even [in BoundedNat.even_half]even [in BoundedNat.bounded_even]
I
is_Ev2_π [in BoundedNat.even_half]is_Ev2 [in BoundedNat.even_half]
is_Ev0 [in BoundedNat.even_half]
is_even_2_π [in BoundedNat.bounded_even]
is_even_2 [in BoundedNat.bounded_even]
is_even_0 [in BoundedNat.bounded_even]
N
no_Ev1 [in BoundedNat.even_half]no_even1 [in BoundedNat.bounded_even]
S
shape_S [in BoundedNat.bounded_nat]shape_O [in BoundedNat.bounded_nat]
T
t [in BoundedNat.bounded_nat]Section Index
S
sec_example [in BoundedNat.bounded_nat]sec_absurd [in BoundedNat.looping_absurd]
Definition Index
D
double_half_in_nat [in BoundedNat.bounded_even]E
evenTF [in BoundedNat.even_half]evenTF_mono [in BoundedNat.even_half]
evenTF_back [in BoundedNat.even_half]
evenTF_unique [in BoundedNat.even_half]
even_rect [in BoundedNat.even_half]
even_inv_π [in BoundedNat.even_half]
even_evenTF [in BoundedNat.even_half]
even_inv [in BoundedNat.even_half]
even_fold [in BoundedNat.bounded_even]
even_rect [in BoundedNat.bounded_even]
even_inv_π [in BoundedNat.bounded_even]
even_lift2 [in BoundedNat.bounded_even]
even_lift1 [in BoundedNat.bounded_even]
even_inv [in BoundedNat.bounded_even]
F
F [in BoundedNat.looping_absurd]Fexc [in BoundedNat.looping_absurd]
Floop [in BoundedNat.looping_absurd]
Floop_F [in BoundedNat.looping_absurd]
Floop_T [in BoundedNat.looping_absurd]
Floop_P [in BoundedNat.looping_absurd]
forget [in BoundedNat.bounded_nat]
Fplus [in BoundedNat.bounded_nat]
fpred2 [in BoundedNat.bounded_even]
H
half [in BoundedNat.even_half]half_in_t_by_fold [in BoundedNat.bounded_even]
half_in_t [in BoundedNat.bounded_even]
half_in_nat [in BoundedNat.bounded_even]
I
iFF_iSS [in BoundedNat.bounded_even]is_FS_FS [in BoundedNat.bounded_even]
is_S_S [in BoundedNat.bounded_even]
L
lift1 [in BoundedNat.bounded_nat]lift2 [in BoundedNat.bounded_even]
loop [in BoundedNat.looping_absurd]
P
P [in BoundedNat.looping_absurd]pr2 [in BoundedNat.bounded_even]
T
T [in BoundedNat.looping_absurd]t_n_Sm [in BoundedNat.bounded_nat]
t_inv [in BoundedNat.bounded_nat]
other
πeven [in BoundedNat.even_half]πeven [in BoundedNat.bounded_even]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (322 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (234 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (41 entries) |
This page has been generated by coqdoc