Global Index

A

G

J

K

M

O

Q

R

U

V

W

X

Y

Z

_

(136 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(4 entries)

Library Index

A

C

D

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Lemma Index

A

B

F

G

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

G

H

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(14 entries)

Inductive Index

A

B

C

D

F

G

H

J

K

L

M

O

P

Q

R

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

T

U

V

W

X

Y

Z

_

other

(2 entries)

Definition Index

A

B

C

G

J

K

M

O

Q

R

U

V

W

X

Y

Z

_

(89 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]

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_sind [definition, in BoundedNat.even_half]
even_ind [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_sind [definition, in BoundedNat.bounded_even]
even_ind [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]

F

F [definition, in BoundedNat.looping_absurd]
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]

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]

I

iFF_iSS [definition, in BoundedNat.bounded_even]
iFF_iSS_inter [lemma, in BoundedNat.bounded_even]
is_Ev2_π_sind [definition, in BoundedNat.even_half]
is_Ev2_π_rec [definition, in BoundedNat.even_half]
is_Ev2_π_ind [definition, in BoundedNat.even_half]
is_Ev2_π_rect [definition, in BoundedNat.even_half]
is_Ev2_π_intro [constructor, in BoundedNat.even_half]
is_Ev2_π [inductive, in BoundedNat.even_half]
is_Ev2_sind [definition, in BoundedNat.even_half]
is_Ev2_rec [definition, in BoundedNat.even_half]
is_Ev2_ind [definition, in BoundedNat.even_half]
is_Ev2_rect [definition, in BoundedNat.even_half]
is_Ev2_intro [constructor, in BoundedNat.even_half]
is_Ev2 [inductive, in BoundedNat.even_half]
is_Ev0_sind [definition, in BoundedNat.even_half]
is_Ev0_rec [definition, in BoundedNat.even_half]
is_Ev0_ind [definition, in BoundedNat.even_half]
is_Ev0_rect [definition, in BoundedNat.even_half]
is_Ev0_intro [constructor, in BoundedNat.even_half]
is_Ev0 [inductive, in BoundedNat.even_half]
is_even_2_π_sind [definition, in BoundedNat.bounded_even]
is_even_2_π_rec [definition, in BoundedNat.bounded_even]
is_even_2_π_ind [definition, in BoundedNat.bounded_even]
is_even_2_π_rect [definition, in BoundedNat.bounded_even]
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_sind [definition, in BoundedNat.bounded_even]
is_even_2_rec [definition, in BoundedNat.bounded_even]
is_even_2_ind [definition, in BoundedNat.bounded_even]
is_even_2_rect [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_sind [definition, in BoundedNat.bounded_even]
is_even_0_rec [definition, in BoundedNat.bounded_even]
is_even_0_ind [definition, in BoundedNat.bounded_even]
is_even_0_rect [definition, in BoundedNat.bounded_even]
is_even_0_intro [constructor, in BoundedNat.bounded_even]
is_even_0 [inductive, 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]

N

no_Ev1_sind [definition, in BoundedNat.even_half]
no_Ev1_rec [definition, in BoundedNat.even_half]
no_Ev1_ind [definition, in BoundedNat.even_half]
no_Ev1_rect [definition, in BoundedNat.even_half]
no_Ev1 [inductive, in BoundedNat.even_half]
no_even1_sind [definition, in BoundedNat.bounded_even]
no_even1_rec [definition, in BoundedNat.bounded_even]
no_even1_ind [definition, in BoundedNat.bounded_even]
no_even1_rect [definition, in BoundedNat.bounded_even]
no_even1 [inductive, in BoundedNat.bounded_even]

P

P [definition, in BoundedNat.looping_absurd]
pr2 [definition, in BoundedNat.bounded_even]

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_sind [definition, in BoundedNat.bounded_nat]
shape_S_rec [definition, in BoundedNat.bounded_nat]
shape_S_ind [definition, in BoundedNat.bounded_nat]
shape_S_rect [definition, in BoundedNat.bounded_nat]
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_sind [definition, in BoundedNat.bounded_nat]
shape_O_rec [definition, in BoundedNat.bounded_nat]
shape_O_ind [definition, in BoundedNat.bounded_nat]
shape_O_rect [definition, 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_sind [definition, in BoundedNat.bounded_nat]
t_rec [definition, in BoundedNat.bounded_nat]
t_ind [definition, in BoundedNat.bounded_nat]
t_rect [definition, in BoundedNat.bounded_nat]

other

πeven [definition, in BoundedNat.even_half]
πeven [definition, in BoundedNat.bounded_even]

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_nat
bounded_even

E

L

Lemma 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_sind [in BoundedNat.even_half]
even_ind [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]
even_sind [in BoundedNat.bounded_even]
even_ind [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_Ev2_π_sind [in BoundedNat.even_half]
is_Ev2_π_rec [in BoundedNat.even_half]
is_Ev2_π_ind [in BoundedNat.even_half]
is_Ev2_π_rect [in BoundedNat.even_half]
is_Ev2_sind [in BoundedNat.even_half]
is_Ev2_rec [in BoundedNat.even_half]
is_Ev2_ind [in BoundedNat.even_half]
is_Ev2_rect [in BoundedNat.even_half]
is_Ev0_sind [in BoundedNat.even_half]
is_Ev0_rec [in BoundedNat.even_half]
is_Ev0_ind [in BoundedNat.even_half]
is_Ev0_rect [in BoundedNat.even_half]
is_even_2_π_sind [in BoundedNat.bounded_even]
is_even_2_π_rec [in BoundedNat.bounded_even]
is_even_2_π_ind [in BoundedNat.bounded_even]
is_even_2_π_rect [in BoundedNat.bounded_even]
is_FS_FS [in BoundedNat.bounded_even]
is_S_S [in BoundedNat.bounded_even]
is_even_2_sind [in BoundedNat.bounded_even]
is_even_2_rec [in BoundedNat.bounded_even]
is_even_2_ind [in BoundedNat.bounded_even]
is_even_2_rect [in BoundedNat.bounded_even]
is_even_0_sind [in BoundedNat.bounded_even]
is_even_0_rec [in BoundedNat.bounded_even]
is_even_0_ind [in BoundedNat.bounded_even]
is_even_0_rect [in BoundedNat.bounded_even]

L

lift1 [in BoundedNat.bounded_nat]
lift2 [in BoundedNat.bounded_even]
loop [in BoundedNat.looping_absurd]

N

no_Ev1_sind [in BoundedNat.even_half]
no_Ev1_rec [in BoundedNat.even_half]
no_Ev1_ind [in BoundedNat.even_half]
no_Ev1_rect [in BoundedNat.even_half]
no_even1_sind [in BoundedNat.bounded_even]
no_even1_rec [in BoundedNat.bounded_even]
no_even1_ind [in BoundedNat.bounded_even]
no_even1_rect [in BoundedNat.bounded_even]

P

P [in BoundedNat.looping_absurd]
pr2 [in BoundedNat.bounded_even]

S

shape_S_sind [in BoundedNat.bounded_nat]
shape_S_rec [in BoundedNat.bounded_nat]
shape_S_ind [in BoundedNat.bounded_nat]
shape_S_rect [in BoundedNat.bounded_nat]
shape_O_sind [in BoundedNat.bounded_nat]
shape_O_rec [in BoundedNat.bounded_nat]
shape_O_ind [in BoundedNat.bounded_nat]
shape_O_rect [in BoundedNat.bounded_nat]

T

T [in BoundedNat.looping_absurd]
t_n_Sm [in BoundedNat.bounded_nat]
t_inv [in BoundedNat.bounded_nat]
t_sind [in BoundedNat.bounded_nat]
t_rec [in BoundedNat.bounded_nat]
t_ind [in BoundedNat.bounded_nat]
t_rect [in BoundedNat.bounded_nat]

other

πeven [in BoundedNat.even_half]
πeven [in BoundedNat.bounded_even]

Global Index

A

G

J

K

M

O

Q

R

U

V

W

X

Y

Z

_

(136 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(4 entries)

Library Index

A

C

D

F

G

H

I

J

K

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Lemma Index

A

B

F

G

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

G

H

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(14 entries)

Inductive Index

A

B

C

D

F

G

H

J

K

L

M

O

P

Q

R

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

T

U

V

W

X

Y

Z

_

other

(2 entries)

Definition Index

A

B

C

G

J

K

M

O

Q

R

U

V

W

X

Y

Z

_

(89 entries)

This page has been generated by coqdoc