Global Index

G

H

J

K

O

Q

R

T

W

X

Y

Z

_

other

(115 entries)

Lemma Index

B

C

G

H

J

K

M

O

Q

R

T

U

V

W

X

Y

Z

_

other

(59 entries)

Constructor Index

A

C

D

F

G

H

J

K

M

N

O

Q

R

T

W

X

Y

Z

_

other

(24 entries)

Inductive Index

A

C

D

F

G

H

J

K

M

N

O

Q

R

T

W

X

Y

Z

_

other

(9 entries)

Definition Index

A

B

D

F

G

H

J

K

N

O

Q

R

T

U

W

X

Y

Z

_

other

(19 entries)

Library Index

A

B

C

D

E

F

G

H

J

K

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Global Index

A

after_loop [lemma, in programming]

B

binoperation [inductive, in programming_machine]
binoperation_get [constructor, in programming_machine]
binoperation_and [constructor, in programming_machine]
binoperation_lt [constructor, in programming_machine]
binoperation_minus [constructor, in programming_machine]
binoperation_plus [constructor, in programming_machine]

C

cast_value_bool [definition, in programming_machine]

D

descending_loop_finishes_general [lemma, in programming]
descending_loop_finishes_general_informative [lemma, in programming]

E

execute [definition, in programming_machine]
execute_app [lemma, in programming]
expression [inductive, in programming_machine]
expression_value [definition, in programming_machine]
exp_binoperation [constructor, in programming_machine]
exp_unioperation [constructor, in programming_machine]
exp_constant [constructor, in programming_machine]
exp_variable [constructor, in programming_machine]

F

finishes_postcondition [lemma, in programming]
finishes_info_app [lemma, in programming]
finishes_loop [lemma, in programming]
finishes_info_loop [lemma, in programming]
finishes_cons [lemma, in programming]
finishes_info_cons [lemma, in programming]
finishes_info_True [lemma, in programming]
firstn_issorted [lemma, in listaux]

I

infinity [lemma, in programming_machine]
insertionsort [definition, in insertionsort]
insertionsort [library]
insertionsort_sorts [lemma, in insertionsort]
insertionsort_permutes [lemma, in insertionsort]
insertionsort_sorted [lemma, in insertionsort]
insertionsort_finishes [lemma, in insertionsort]
insertionsort_invariant_1lower [lemma, in insertionsort]
insertionsort_preservedtype [lemma, in insertionsort]
invariant [definition, in programming]
invariant_postcondition [lemma, in programming]
invariant_cons_destroy [lemma, in programming]
invariant_loop_iterations [lemma, in programming]
invariant_loop_iterations_informative [lemma, in programming]
invariant_loop [lemma, in programming]
invariant_loop_informative [lemma, in programming]
invariant_cons [lemma, in programming]
invariant_cons_execute [lemma, in programming]
invariant_nil [lemma, in programming]
issorted [inductive, in listaux]
issorted_firstn_S [lemma, in listaux]
issorted_skip [lemma, in listaux]
issorted_12345 [lemma, in listaux]
issorted_cons [constructor, in listaux]
issorted_single [constructor, in listaux]
issorted_nil [constructor, in listaux]

L

listaux [library]
loop [inductive, in programming_machine]
loop_iterations_induction [lemma, in programming]
loop_greater_limit [lemma, in programming]
loop_program_rect [definition, in programming_machine]
loop_nil [lemma, in programming_machine]
loop_execute [definition, in programming_machine]
loop_intro [constructor, in programming_machine]

M

memory [definition, in programming_machine]

N

nth_set_same [lemma, in listaux]

P

Permutation_set_displacement [lemma, in listaux]
Permutation_nil_r [lemma, in listaux]
Permutation_nil_l [lemma, in listaux]
permutation12345 [lemma, in listaux]
postcondition [definition, in programming]
postcondition_loop_iterations_special [lemma, in programming]
postcondition_loop_iterations_informative [lemma, in programming]
postcondition_loop_general [lemma, in programming]
postcondition_cons [lemma, in programming]
postcondition_nil [lemma, in programming]
program [inductive, in programming_machine]
programming [library]
programming_machine [library]
program_sorts [definition, in programming]
program_app_finishes_destroy [lemma, in programming]
program_finishes_info [definition, in programming]
program_finishes [definition, in programming]
program_chain_greater_limit [lemma, in programming]
program_chain [definition, in programming]
program_greater_limit [lemma, in programming]
program_app_postcondition [lemma, in programming]
program_app_invariant_informative [lemma, in programming]
program_app_loop_fold [lemma, in programming]
program_app_cons_fold [lemma, in programming]
program_app_nil_r [lemma, in programming]
program_app_nil_l [lemma, in programming]
program_app [definition, in programming]
program_rect_expanded [lemma, in programming_machine]
program_loop_rect [definition, in programming_machine]
program_loop [constructor, in programming_machine]
program_cons [constructor, in programming_machine]
program_nil [constructor, in programming_machine]

S

set [definition, in listaux]
setandraise [definition, in listaux]
setandraise_equallength [lemma, in listaux]
setandraise_longer [lemma, in listaux]
setandraise_set [lemma, in listaux]
set_nth_different [lemma, in listaux]
set_nth_same [lemma, in listaux]
statement [inductive, in programming_machine]
statement_execute [definition, in programming_machine]
statement_listset [constructor, in programming_machine]
statement_assignment [constructor, in programming_machine]

U

unioperation [inductive, in programming_machine]
unioperation_len [constructor, in programming_machine]

V

value [inductive, in programming_machine]
value_listnat [constructor, in programming_machine]
value_nat [constructor, in programming_machine]
value_none [constructor, in programming_machine]
variable [inductive, in programming_machine]
variable_value [definition, in programming_machine]
var_scope [constructor, in programming_machine]
var_argument [constructor, in programming_machine]

Lemma Index

A

after_loop [in programming]

D

descending_loop_finishes_general [in programming]
descending_loop_finishes_general_informative [in programming]

E

execute_app [in programming]

F

finishes_postcondition [in programming]
finishes_info_app [in programming]
finishes_loop [in programming]
finishes_info_loop [in programming]
finishes_cons [in programming]
finishes_info_cons [in programming]
finishes_info_True [in programming]
firstn_issorted [in listaux]

I

infinity [in programming_machine]
insertionsort_sorts [in insertionsort]
insertionsort_permutes [in insertionsort]
insertionsort_sorted [in insertionsort]
insertionsort_finishes [in insertionsort]
insertionsort_invariant_1lower [in insertionsort]
insertionsort_preservedtype [in insertionsort]
invariant_postcondition [in programming]
invariant_cons_destroy [in programming]
invariant_loop_iterations [in programming]
invariant_loop_iterations_informative [in programming]
invariant_loop [in programming]
invariant_loop_informative [in programming]
invariant_cons [in programming]
invariant_cons_execute [in programming]
invariant_nil [in programming]
issorted_firstn_S [in listaux]
issorted_skip [in listaux]
issorted_12345 [in listaux]

L

loop_iterations_induction [in programming]
loop_greater_limit [in programming]
loop_nil [in programming_machine]

N

nth_set_same [in listaux]

P

Permutation_set_displacement [in listaux]
Permutation_nil_r [in listaux]
Permutation_nil_l [in listaux]
permutation12345 [in listaux]
postcondition_loop_iterations_special [in programming]
postcondition_loop_iterations_informative [in programming]
postcondition_loop_general [in programming]
postcondition_cons [in programming]
postcondition_nil [in programming]
program_app_finishes_destroy [in programming]
program_chain_greater_limit [in programming]
program_greater_limit [in programming]
program_app_postcondition [in programming]
program_app_invariant_informative [in programming]
program_app_loop_fold [in programming]
program_app_cons_fold [in programming]
program_app_nil_r [in programming]
program_app_nil_l [in programming]
program_rect_expanded [in programming_machine]

S

setandraise_equallength [in listaux]
setandraise_longer [in listaux]
setandraise_set [in listaux]
set_nth_different [in listaux]
set_nth_same [in listaux]

Constructor Index

B

binoperation_get [in programming_machine]
binoperation_and [in programming_machine]
binoperation_lt [in programming_machine]
binoperation_minus [in programming_machine]
binoperation_plus [in programming_machine]

E

exp_binoperation [in programming_machine]
exp_unioperation [in programming_machine]
exp_constant [in programming_machine]
exp_variable [in programming_machine]

I

issorted_cons [in listaux]
issorted_single [in listaux]
issorted_nil [in listaux]

L

loop_intro [in programming_machine]

P

program_loop [in programming_machine]
program_cons [in programming_machine]
program_nil [in programming_machine]

S

statement_listset [in programming_machine]
statement_assignment [in programming_machine]

U

unioperation_len [in programming_machine]

V

value_listnat [in programming_machine]
value_nat [in programming_machine]
value_none [in programming_machine]
var_scope [in programming_machine]
var_argument [in programming_machine]

Inductive Index

B

binoperation [in programming_machine]

E

expression [in programming_machine]

I

issorted [in listaux]

L

loop [in programming_machine]

P

program [in programming_machine]

S

statement [in programming_machine]

U

unioperation [in programming_machine]

V

value [in programming_machine]
variable [in programming_machine]

Definition Index

C

cast_value_bool [in programming_machine]

E

execute [in programming_machine]
expression_value [in programming_machine]

I

insertionsort [in insertionsort]
invariant [in programming]

L

loop_program_rect [in programming_machine]
loop_execute [in programming_machine]

M

memory [in programming_machine]

P

postcondition [in programming]
program_sorts [in programming]
program_finishes_info [in programming]
program_finishes [in programming]
program_chain [in programming]
program_app [in programming]
program_loop_rect [in programming_machine]

S

set [in listaux]
setandraise [in listaux]
statement_execute [in programming_machine]

V

variable_value [in programming_machine]

Library Index

I

L

P

programming
programming_machine

Global Index

G

H

J

K

O

Q

R

T

W

X

Y

Z

_

other

(115 entries)

Lemma Index

B

C

G

H

J

K

M

O

Q

R

T

U

V

W

X

Y

Z

_

other

(59 entries)

Constructor Index

A

C

D

F

G

H

J

K

M

N

O

Q

R

T

W

X

Y

Z

_

other

(24 entries)

Inductive Index

A

C

D

F

G

H

J

K

M

N

O

Q

R

T

W

X

Y

Z

_

other

(9 entries)

Definition Index

A

B

D

F

G

H

J

K

N

O

Q

R

T

U

W

X

Y

Z

_

other

(19 entries)

Library Index

A

B

C

D

E

F

G

H

J

K

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

This page has been generated by coqdoc