| 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 |
_ |
(169 entries) |
| Tactic 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 |
_ |
(10 entries) |
| Axiom 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 |
_ |
(13 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 |
_ |
(47 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 |
_ |
(20 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 |
_ |
(12 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 |
_ |
(51 entries) |
| Module 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 |
_ |
(16 entries) |
Global Index
A
access [definition, in ...lib.coq.WhyArrays]
AccessOther [tactic definition, in ...lib.coq.WhyArrays]
AccessSame [tactic definition, in ...lib.coq.WhyArrays]
AccessStore [tactic definition, in ...lib.coq.WhyArrays]
annot_bool [definition, in ...lib.coq.WhyBool]
array [definition, in ...lib.coq.WhyArrays]
ArrayLength [tactic definition, in ...lib.coq.WhyTactics]
ArraySubst [tactic definition, in ...lib.coq.WhyArrays]
array_id [definition, in ...lib.coq.WhyPermut]
array_id_refl [lemma, in ...lib.coq.WhyPermut]
array_id_sym [lemma, in ...lib.coq.WhyPermut]
array_id_trans [lemma, in ...lib.coq.WhyPermut]
array_length [definition, in ...lib.coq.WhyArrays]
array_length_store [lemma, in ...lib.coq.WhyArrays]
B
bool_of_sumbool [definition, in ...lib.coq.WhyCoq73]
btest [definition, in ...lib.coq.WhyBool]
Build_tuple_2 [definition, in ...lib.coq.WhyTuples]
B_eq_bool [definition, in ...lib.coq.WhyBool]
B_eq_dec [definition, in ...lib.coq.WhyBool]
B_noteq_bool [definition, in ...lib.coq.WhyBool]
C
CallSubst [tactic definition, in ...lib.coq.WhyTactics]
D
decomp [definition, in ...lib.coq.WhyExn]
decomp1 [definition, in ...lib.coq.WhyExn]
decomp2 [definition, in ...lib.coq.WhyExn]
decomp3 [definition, in ...lib.coq.WhyExn]
decomp4 [definition, in ...lib.coq.WhyExn]
E
EM [inductive, in ...lib.coq.WhyExn]
exchange [inductive, in ...lib.coq.WhyPermut]
exchange_c [constructor, in ...lib.coq.WhyPermut]
exchange_id [lemma, in ...lib.coq.WhyPermut]
exchange_is_permut [constructor, in ...lib.coq.WhyPermut]
exchange_is_sub_permut [constructor, in ...lib.coq.WhyPermut]
exchange_length [lemma, in ...lib.coq.WhyPermut]
exchange_proof [lemma, in ...lib.coq.WhyPermut]
exchange_sym [lemma, in ...lib.coq.WhyPermut]
exchange_1 [lemma, in ...lib.coq.WhyPermut]
exist_1 [definition, in ...lib.coq.WhyTuples]
exist_2 [constructor, in ...lib.coq.WhyTuples]
exist_3 [constructor, in ...lib.coq.WhyTuples]
exist_4 [constructor, in ...lib.coq.WhyTuples]
exist_5 [constructor, in ...lib.coq.WhyTuples]
exist_6 [constructor, in ...lib.coq.WhyTuples]
exist_7 [constructor, in ...lib.coq.WhyTuples]
exist_8 [constructor, in ...lib.coq.WhyTuples]
Exn [constructor, in ...lib.coq.WhyExn]
I
if_then_else [definition, in ...lib.coq.WhyBool]
iter_sqrt_invar1 [lemma, in sqrt.sqrt_why]
iter_sqrt_invar2 [lemma, in sqrt.sqrt_why]
iter_sqrt_invar3 [lemma, in sqrt.sqrt_why]
iter_sqrt_invar4 [lemma, in sqrt.sqrt_why]
iter_sqrt_pos [lemma, in sqrt.sqrt_why]
iter_sqrt_pos2 [lemma, in sqrt.sqrt_why]
L
left_extension [lemma, in ...lib.coq.WhySorted]
left_substitution [lemma, in ...lib.coq.WhySorted]
loop_variant_1 [lemma, in ...lib.coq.WhyLemmas]
lt_ge_dec [definition, in ...lib.coq.WhyCoq73]
N
nat_eq_bool [definition, in ...lib.coq.WhyCoq73]
nat_ge_lt_bool [definition, in ...lib.coq.WhyCoq73]
nat_gt_le_bool [definition, in ...lib.coq.WhyCoq73]
nat_le_gt_bool [definition, in ...lib.coq.WhyCoq73]
nat_lt_ge_bool [definition, in ...lib.coq.WhyCoq73]
nat_noteq_bool [definition, in ...lib.coq.WhyCoq73]
new [definition, in ...lib.coq.WhyArrays]
new_def [axiom, in ...lib.coq.WhyArrays]
notzerop [definition, in ...lib.coq.WhyCoq73]
notzerop_bool [definition, in ...lib.coq.WhyCoq73]
no_effect [lemma, in ...lib.coq.WhySorted]
P
permut [inductive, in ...lib.coq.WhyPermut]
permut_length [lemma, in ...lib.coq.WhyPermut]
permut_refl [constructor, in ...lib.coq.WhyPermut]
permut_sym [constructor, in ...lib.coq.WhyPermut]
permut_trans [constructor, in ...lib.coq.WhyPermut]
prog_bool_and [definition, in ...lib.coq.WhyBool]
prog_bool_not [definition, in ...lib.coq.WhyBool]
prog_bool_or [definition, in ...lib.coq.WhyBool]
proj_2_1 [definition, in ...lib.coq.WhyTuples]
proj_2_2 [definition, in ...lib.coq.WhyTuples]
ProveSameLength [tactic definition, in ...lib.coq.WhyTactics]
ProveSameLengthSym [tactic definition, in ...lib.coq.WhyTactics]
Q
qcomb [definition, in ...lib.coq.WhyExn]
QEM [inductive, in ...lib.coq.WhyExn]
QEM_mon [definition, in ...lib.coq.WhyExn]
Qexn [constructor, in ...lib.coq.WhyExn]
Qval [constructor, in ...lib.coq.WhyExn]
R
raw_access [axiom, in ...lib.coq.WhyArrays]
raw_array [axiom, in ...lib.coq.WhyArrays]
raw_new [axiom, in ...lib.coq.WhyArrays]
raw_store [axiom, in ...lib.coq.WhyArrays]
right_extension [lemma, in ...lib.coq.WhySorted]
right_substitution [lemma, in ...lib.coq.WhySorted]
R_eq_bool [axiom, in ...lib.coq.WhyFloat]
R_ge_lt_bool [axiom, in ...lib.coq.WhyFloat]
R_gt_le_bool [axiom, in ...lib.coq.WhyFloat]
R_le_gt_bool [axiom, in ...lib.coq.WhyFloat]
R_lt_ge_bool [axiom, in ...lib.coq.WhyFloat]
R_noteq_bool [axiom, in ...lib.coq.WhyFloat]
S
SameLength [tactic definition, in ...lib.coq.WhyTactics]
sig_1 [definition, in ...lib.coq.WhyTuples]
sig_2 [inductive, in ...lib.coq.WhyTuples]
sig_3 [inductive, in ...lib.coq.WhyTuples]
sig_4 [inductive, in ...lib.coq.WhyTuples]
sig_5 [inductive, in ...lib.coq.WhyTuples]
sig_6 [inductive, in ...lib.coq.WhyTuples]
sig_7 [inductive, in ...lib.coq.WhyTuples]
sig_8 [inductive, in ...lib.coq.WhyTuples]
sorted_array [definition, in ...lib.coq.WhySorted]
sorted_array_id [lemma, in ...lib.coq.WhySorted]
sorted_elements [lemma, in ...lib.coq.WhySorted]
sorted_elements_1 [lemma, in ...lib.coq.WhySorted]
spec_and [definition, in ...lib.coq.WhyBool]
spec_not [definition, in ...lib.coq.WhyBool]
spec_or [definition, in ...lib.coq.WhyBool]
sqrt [definition, in sqrt.sqrt_valid]
sqrt_po_1 [lemma, in sqrt.sqrt_why]
sqrt_po_2 [lemma, in sqrt.sqrt_why]
sqrt_po_3 [lemma, in sqrt.sqrt_why]
sqrt_po_4 [lemma, in sqrt.sqrt_why]
sqrt_po_5 [lemma, in sqrt.sqrt_why]
sqrt_po_6 [lemma, in sqrt.sqrt_why]
sqrt_valid [module]
sqrt_why [module]
sqr_gt [lemma, in sqrt.sqrt_why]
store [definition, in ...lib.coq.WhyArrays]
store_def_1 [axiom, in ...lib.coq.WhyArrays]
store_def_2 [axiom, in ...lib.coq.WhyArrays]
sub_permut [inductive, in ...lib.coq.WhyPermut]
sub_permut_eq [lemma, in ...lib.coq.WhyPermut]
sub_permut_extension [lemma, in ...lib.coq.WhyPermut]
sub_permut_function [lemma, in ...lib.coq.WhyPermut]
sub_permut_id [lemma, in ...lib.coq.WhyPermut]
sub_permut_is_permut [lemma, in ...lib.coq.WhyPermut]
sub_permut_length [lemma, in ...lib.coq.WhyPermut]
sub_permut_refl [constructor, in ...lib.coq.WhyPermut]
sub_permut_sym [constructor, in ...lib.coq.WhyPermut]
sub_permut_trans [constructor, in ...lib.coq.WhyPermut]
sub_permut_void [lemma, in ...lib.coq.WhyPermut]
sub_sorted_array [lemma, in ...lib.coq.WhySorted]
T
tuple_1 [definition, in ...lib.coq.WhyTuples]
tuple_2 [definition, in ...lib.coq.WhyTuples]
U
uncurry [definition, in ...lib.coq.WhyExn]
U_eq_bool [definition, in ...lib.coq.WhyBool]
U_eq_dec [definition, in ...lib.coq.WhyBool]
U_noteq_bool [definition, in ...lib.coq.WhyBool]
V
Val [constructor, in ...lib.coq.WhyExn]
W
Why [module]
WhyArrays [tactic definition, in ...lib.coq.WhyArrays]
WhyArrays [module]
WhyBool [module]
WhyCoqCompat [module]
WhyCoqDev [module]
WhyCoq73 [module]
WhyExn [module]
WhyFloat [module]
WhyInt [module]
WhyLemmas [module]
WhyPermut [module]
WhySorted [module]
WhyTactics [module]
WhyTuples [module]
why_boolean_case [lemma, in ...lib.coq.WhyLemmas]
why_rewrite_var [lemma, in ...lib.coq.WhyLemmas]
Z
zerop_bool [definition, in ...lib.coq.WhyCoq73]
Znotzero [lemma, in ...lib.coq.WhyInt]
Zwf [definition, in ...lib.coq.WhyCoq73]
Zwf_up [definition, in ...lib.coq.WhyCoq73]
Zwf_up_well_founded [lemma, in ...lib.coq.WhyCoq73]
Zwf_well_founded [lemma, in ...lib.coq.WhyCoq73]
Z_div_same [lemma, in sqrt.sqrt_why]
Z_mod_same [lemma, in sqrt.sqrt_why]
Tactic Index
A
AccessOther [in ...lib.coq.WhyArrays]
AccessSame [in ...lib.coq.WhyArrays]
AccessStore [in ...lib.coq.WhyArrays]
ArrayLength [in ...lib.coq.WhyTactics]
ArraySubst [in ...lib.coq.WhyArrays]
C
CallSubst [in ...lib.coq.WhyTactics]
P
ProveSameLength [in ...lib.coq.WhyTactics]
ProveSameLengthSym [in ...lib.coq.WhyTactics]
S
SameLength [in ...lib.coq.WhyTactics]
W
WhyArrays [in ...lib.coq.WhyArrays]
Axiom Index
N
new_def [in ...lib.coq.WhyArrays]
R
raw_access [in ...lib.coq.WhyArrays]
raw_array [in ...lib.coq.WhyArrays]
raw_new [in ...lib.coq.WhyArrays]
raw_store [in ...lib.coq.WhyArrays]
R_eq_bool [in ...lib.coq.WhyFloat]
R_ge_lt_bool [in ...lib.coq.WhyFloat]
R_gt_le_bool [in ...lib.coq.WhyFloat]
R_le_gt_bool [in ...lib.coq.WhyFloat]
R_lt_ge_bool [in ...lib.coq.WhyFloat]
R_noteq_bool [in ...lib.coq.WhyFloat]
S
store_def_1 [in ...lib.coq.WhyArrays]
store_def_2 [in ...lib.coq.WhyArrays]
Lemma Index
A
array_id_refl [in ...lib.coq.WhyPermut]
array_id_sym [in ...lib.coq.WhyPermut]
array_id_trans [in ...lib.coq.WhyPermut]
array_length_store [in ...lib.coq.WhyArrays]
E
exchange_id [in ...lib.coq.WhyPermut]
exchange_length [in ...lib.coq.WhyPermut]
exchange_proof [in ...lib.coq.WhyPermut]
exchange_sym [in ...lib.coq.WhyPermut]
exchange_1 [in ...lib.coq.WhyPermut]
I
iter_sqrt_invar1 [in sqrt.sqrt_why]
iter_sqrt_invar2 [in sqrt.sqrt_why]
iter_sqrt_invar3 [in sqrt.sqrt_why]
iter_sqrt_invar4 [in sqrt.sqrt_why]
iter_sqrt_pos [in sqrt.sqrt_why]
iter_sqrt_pos2 [in sqrt.sqrt_why]
L
left_extension [in ...lib.coq.WhySorted]
left_substitution [in ...lib.coq.WhySorted]
loop_variant_1 [in ...lib.coq.WhyLemmas]
N
no_effect [in ...lib.coq.WhySorted]
P
permut_length [in ...lib.coq.WhyPermut]
R
right_extension [in ...lib.coq.WhySorted]
right_substitution [in ...lib.coq.WhySorted]
S
sorted_array_id [in ...lib.coq.WhySorted]
sorted_elements [in ...lib.coq.WhySorted]
sorted_elements_1 [in ...lib.coq.WhySorted]
sqrt_po_1 [in sqrt.sqrt_why]
sqrt_po_2 [in sqrt.sqrt_why]
sqrt_po_3 [in sqrt.sqrt_why]
sqrt_po_4 [in sqrt.sqrt_why]
sqrt_po_5 [in sqrt.sqrt_why]
sqrt_po_6 [in sqrt.sqrt_why]
sqr_gt [in sqrt.sqrt_why]
sub_permut_eq [in ...lib.coq.WhyPermut]
sub_permut_extension [in ...lib.coq.WhyPermut]
sub_permut_function [in ...lib.coq.WhyPermut]
sub_permut_id [in ...lib.coq.WhyPermut]
sub_permut_is_permut [in ...lib.coq.WhyPermut]
sub_permut_length [in ...lib.coq.WhyPermut]
sub_permut_void [in ...lib.coq.WhyPermut]
sub_sorted_array [in ...lib.coq.WhySorted]
W
why_boolean_case [in ...lib.coq.WhyLemmas]
why_rewrite_var [in ...lib.coq.WhyLemmas]
Z
Znotzero [in ...lib.coq.WhyInt]
Zwf_up_well_founded [in ...lib.coq.WhyCoq73]
Zwf_well_founded [in ...lib.coq.WhyCoq73]
Z_div_same [in sqrt.sqrt_why]
Z_mod_same [in sqrt.sqrt_why]
Constructor Index
E
exchange_c [in ...lib.coq.WhyPermut]
exchange_is_permut [in ...lib.coq.WhyPermut]
exchange_is_sub_permut [in ...lib.coq.WhyPermut]
exist_2 [in ...lib.coq.WhyTuples]
exist_3 [in ...lib.coq.WhyTuples]
exist_4 [in ...lib.coq.WhyTuples]
exist_5 [in ...lib.coq.WhyTuples]
exist_6 [in ...lib.coq.WhyTuples]
exist_7 [in ...lib.coq.WhyTuples]
exist_8 [in ...lib.coq.WhyTuples]
Exn [in ...lib.coq.WhyExn]
P
permut_refl [in ...lib.coq.WhyPermut]
permut_sym [in ...lib.coq.WhyPermut]
permut_trans [in ...lib.coq.WhyPermut]
Q
Qexn [in ...lib.coq.WhyExn]
Qval [in ...lib.coq.WhyExn]
S
sub_permut_refl [in ...lib.coq.WhyPermut]
sub_permut_sym [in ...lib.coq.WhyPermut]
sub_permut_trans [in ...lib.coq.WhyPermut]
V
Val [in ...lib.coq.WhyExn]
Inductive Index
E
EM [in ...lib.coq.WhyExn]
exchange [in ...lib.coq.WhyPermut]
P
permut [in ...lib.coq.WhyPermut]
Q
QEM [in ...lib.coq.WhyExn]
S
sig_2 [in ...lib.coq.WhyTuples]
sig_3 [in ...lib.coq.WhyTuples]
sig_4 [in ...lib.coq.WhyTuples]
sig_5 [in ...lib.coq.WhyTuples]
sig_6 [in ...lib.coq.WhyTuples]
sig_7 [in ...lib.coq.WhyTuples]
sig_8 [in ...lib.coq.WhyTuples]
sub_permut [in ...lib.coq.WhyPermut]
Definition Index
A
access [in ...lib.coq.WhyArrays]
annot_bool [in ...lib.coq.WhyBool]
array [in ...lib.coq.WhyArrays]
array_id [in ...lib.coq.WhyPermut]
array_length [in ...lib.coq.WhyArrays]
B
bool_of_sumbool [in ...lib.coq.WhyCoq73]
btest [in ...lib.coq.WhyBool]
Build_tuple_2 [in ...lib.coq.WhyTuples]
B_eq_bool [in ...lib.coq.WhyBool]
B_eq_dec [in ...lib.coq.WhyBool]
B_noteq_bool [in ...lib.coq.WhyBool]
D
decomp [in ...lib.coq.WhyExn]
decomp1 [in ...lib.coq.WhyExn]
decomp2 [in ...lib.coq.WhyExn]
decomp3 [in ...lib.coq.WhyExn]
decomp4 [in ...lib.coq.WhyExn]
E
exist_1 [in ...lib.coq.WhyTuples]
I
if_then_else [in ...lib.coq.WhyBool]
L
lt_ge_dec [in ...lib.coq.WhyCoq73]
N
nat_eq_bool [in ...lib.coq.WhyCoq73]
nat_ge_lt_bool [in ...lib.coq.WhyCoq73]
nat_gt_le_bool [in ...lib.coq.WhyCoq73]
nat_le_gt_bool [in ...lib.coq.WhyCoq73]
nat_lt_ge_bool [in ...lib.coq.WhyCoq73]
nat_noteq_bool [in ...lib.coq.WhyCoq73]
new [in ...lib.coq.WhyArrays]
notzerop [in ...lib.coq.WhyCoq73]
notzerop_bool [in ...lib.coq.WhyCoq73]
P
prog_bool_and [in ...lib.coq.WhyBool]
prog_bool_not [in ...lib.coq.WhyBool]
prog_bool_or [in ...lib.coq.WhyBool]
proj_2_1 [in ...lib.coq.WhyTuples]
proj_2_2 [in ...lib.coq.WhyTuples]
Q
qcomb [in ...lib.coq.WhyExn]
QEM_mon [in ...lib.coq.WhyExn]
S
sig_1 [in ...lib.coq.WhyTuples]
sorted_array [in ...lib.coq.WhySorted]
spec_and [in ...lib.coq.WhyBool]
spec_not [in ...lib.coq.WhyBool]
spec_or [in ...lib.coq.WhyBool]
sqrt [in sqrt.sqrt_valid]
store [in ...lib.coq.WhyArrays]
T
tuple_1 [in ...lib.coq.WhyTuples]
tuple_2 [in ...lib.coq.WhyTuples]
U
uncurry [in ...lib.coq.WhyExn]
U_eq_bool [in ...lib.coq.WhyBool]
U_eq_dec [in ...lib.coq.WhyBool]
U_noteq_bool [in ...lib.coq.WhyBool]
Z
zerop_bool [in ...lib.coq.WhyCoq73]
Zwf [in ...lib.coq.WhyCoq73]
Zwf_up [in ...lib.coq.WhyCoq73]
Module Index
S
sqrt_valid
sqrt_why
W
Why
WhyArrays
WhyBool
WhyCoqCompat
WhyCoqDev
WhyCoq73
WhyExn
WhyFloat
WhyInt
WhyLemmas
WhyPermut
WhySorted
WhyTactics
WhyTuples
| 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 |
_ |
(169 entries) |
| Tactic 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 |
_ |
(10 entries) |
| Axiom 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 |
_ |
(13 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 |
_ |
(47 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 |
_ |
(20 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 |
_ |
(12 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 |
_ |
(51 entries) |
| Module 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 |
_ |
(16 entries) |
This page has been generated by coqdoc