Global Index

B

K

Q

X

Y

Z

_

other

(416 entries)

Variable Index

A

B

D

E

F

G

H

I

J

K

M

N

Q

R

S

T

V

W

X

Y

Z

_

other

(22 entries)

Library Index

A

B

C

E

F

G

H

I

J

K

M

N

Q

R

V

W

X

Y

Z

_

other

(9 entries)

Lemma Index

B

K

Q

X

Y

Z

_

other

(254 entries)

Constructor Index

A

B

C

D

F

H

I

J

K

M

N

Q

R

S

T

W

X

Y

Z

_

other

(14 entries)

Inductive Index

A

B

D

E

F

G

H

I

J

K

M

N

Q

R

S

T

V

W

X

Y

Z

_

other

(6 entries)

Section Index

A

B

D

E

F

G

H

I

J

K

M

N

Q

R

S

T

V

W

X

Y

Z

_

other

(6 entries)

Definition Index

B

H

K

Q

W

X

Y

Z

_

other

(105 entries)

Global Index

A

add [definition, in Sudoku.OrderedList]
add_inv [lemma, in Sudoku.OrderedList]
add_incl_r [lemma, in Sudoku.OrderedList]
add_incl_l [lemma, in Sudoku.OrderedList]
add_length [lemma, in Sudoku.OrderedList]
add_cont [definition, in Sudoku.OrderedList]
all_cell_sat [lemma, in Sudoku.Sudoku]
all_cell_ordered [lemma, in Sudoku.Sudoku]
all_cell [definition, in Sudoku.Sudoku]
all_permutations_permutation [lemma, in Sudoku.Permutation]
all_permutations [definition, in Sudoku.Permutation]
all_permutations_aux [definition, in Sudoku.Permutation]
anti_literals_sat [lemma, in Sudoku.Sudoku]
anti_literals_in [lemma, in Sudoku.Sudoku]
anti_literals_ordered [lemma, in Sudoku.Sudoku]
anti_literals [definition, in Sudoku.Sudoku]
app_inv_app2 [lemma, in Sudoku.ListAux]
app_inv_app [lemma, in Sudoku.ListAux]
app_inv_tail [lemma, in Sudoku.ListAux]
app_inv_head [lemma, in Sudoku.ListAux]
A_dec [definition, in Sudoku.OrderedList]

C

check [definition, in Sudoku.Sudoku]
check [section, in Sudoku.Sudoku]
check_P [definition, in Sudoku.Sudoku]
check.h [variable, in Sudoku.Sudoku]
check.w [variable, in Sudoku.Sudoku]
clause [definition, in Sudoku.Sudoku]
clauses [definition, in Sudoku.Sudoku]
clauses_update_sat_rev [lemma, in Sudoku.Sudoku]
clauses_update_sat [lemma, in Sudoku.Sudoku]
clauses_merge_sat [lemma, in Sudoku.Sudoku]
clauses_update_valid [lemma, in Sudoku.Sudoku]
clauses_merge_valid [lemma, in Sudoku.Sudoku]
clauses_update_ordered [lemma, in Sudoku.Sudoku]
clauses_merge_in [lemma, in Sudoku.Sudoku]
clauses_update [definition, in Sudoku.Sudoku]
clauses_merge [definition, in Sudoku.Sudoku]
clause_insert_sat [lemma, in Sudoku.Sudoku]
clause_sat [definition, in Sudoku.Sudoku]
clause_insert_valid [lemma, in Sudoku.Sudoku]
clause_merge_valid [lemma, in Sudoku.Sudoku]
clause_insert_ordered [lemma, in Sudoku.Sudoku]
clause_merge_ordered [lemma, in Sudoku.Sudoku]
clause_insert_in [lemma, in Sudoku.Sudoku]
clause_merge_in [lemma, in Sudoku.Sudoku]
clause_insert [definition, in Sudoku.Sudoku]
clause_merge [definition, in Sudoku.Sudoku]
clause_test [definition, in Sudoku.Sudoku]
cmp [inductive, in Sudoku.OrderedList]
column [definition, in Sudoku.Sudoku]
cross [definition, in Sudoku.Sudoku]
cross_correct [lemma, in Sudoku.Sudoku]
cross1 [definition, in Sudoku.Sudoku]
cross1_correct [lemma, in Sudoku.Sudoku]
cross2 [definition, in Sudoku.Sudoku]
cross2_correct [lemma, in Sudoku.Sudoku]

D

div [definition, in Sudoku.Div]
Div [library]
div_mult_comp [lemma, in Sudoku.Div]
div_is_0 [lemma, in Sudoku.Div]
div_lt [lemma, in Sudoku.Div]
div_mod_correct [lemma, in Sudoku.Div]
div_mod_aux_correct [lemma, in Sudoku.Div]
div_aux [definition, in Sudoku.Div]

E

empty [definition, in Sudoku.Sudoku]
empty_take [lemma, in Sudoku.Sudoku]
empty_inv [lemma, in Sudoku.Sudoku]
empty_cons [lemma, in Sudoku.Sudoku]
empty_jump [lemma, in Sudoku.Sudoku]
empty_mk_0 [lemma, in Sudoku.Sudoku]
empty_nil [lemma, in Sudoku.Sudoku]
eq [constructor, in Sudoku.OrderedList]
eq_nat [definition, in Sudoku.OrderedList]

F

find_all_correct [lemma, in Sudoku.Sudoku]
find_one_correct [lemma, in Sudoku.Sudoku]
find_all_aux_sat [lemma, in Sudoku.Sudoku]
find_one_aux_sat [lemma, in Sudoku.Sudoku]
find_all [definition, in Sudoku.Sudoku]
find_all_aux [definition, in Sudoku.Sudoku]
find_one [definition, in Sudoku.Sudoku]
find_one_aux [definition, in Sudoku.Sudoku]
fold_clause_insert3 [lemma, in Sudoku.Sudoku]
fold_clause_insert2 [lemma, in Sudoku.Sudoku]
fold_clause_insert1 [lemma, in Sudoku.Sudoku]
fold_clause_insert_ordered [lemma, in Sudoku.Sudoku]
fold_insert2 [lemma, in Sudoku.Sudoku]
fold_insert1 [lemma, in Sudoku.Sudoku]

G

gen_cell_sat [lemma, in Sudoku.Sudoku]
gen_rect_sat [lemma, in Sudoku.Sudoku]
gen_column_sat [lemma, in Sudoku.Sudoku]
gen_row_sat [lemma, in Sudoku.Sudoku]
gen_init_clauses_valid [lemma, in Sudoku.Sudoku]
gen_init_clauses_ordered [lemma, in Sudoku.Sudoku]
gen_cell_ordered [lemma, in Sudoku.Sudoku]
gen_rect_ordered [lemma, in Sudoku.Sudoku]
gen_column_ordered [lemma, in Sudoku.Sudoku]
gen_row_ordered [lemma, in Sudoku.Sudoku]
gen_cell_correct [lemma, in Sudoku.Sudoku]
gen_rect_correct [lemma, in Sudoku.Sudoku]
gen_column_correct [lemma, in Sudoku.Sudoku]
gen_row_correct [lemma, in Sudoku.Sudoku]
gen_init_clauses [definition, in Sudoku.Sudoku]
gen_init_clauses_aux [definition, in Sudoku.Sudoku]
gen_cell [definition, in Sudoku.Sudoku]
gen_rect [definition, in Sudoku.Sudoku]
gen_column [definition, in Sudoku.Sudoku]
gen_row [definition, in Sudoku.Sudoku]
get [definition, in Sudoku.Sudoku]
get_rect [lemma, in Sudoku.Sudoku]
get_column [lemma, in Sudoku.Sudoku]
get_row [lemma, in Sudoku.Sudoku]
get_mk_0 [lemma, in Sudoku.Sudoku]
get_next [lemma, in Sudoku.Sudoku]
get_nil [lemma, in Sudoku.Sudoku]
gt [constructor, in Sudoku.OrderedList]

H

h_pos [lemma, in Sudoku.Sudoku]

I

incl_length_repetition [lemma, in Sudoku.UList]
indexes [definition, in Sudoku.Sudoku]
init [definition, in Sudoku.Sudoku]
init_c_sudoku [lemma, in Sudoku.Sudoku]
init_c_sat [lemma, in Sudoku.Sudoku]
init_c_ordered [lemma, in Sudoku.Sudoku]
init_c [definition, in Sudoku.Sudoku]
insert [definition, in Sudoku.OrderedList]
insert_cont [definition, in Sudoku.OrderedList]
insert_olist [lemma, in Sudoku.OrderedList]
insert_inv [lemma, in Sudoku.OrderedList]
insert_incl [lemma, in Sudoku.OrderedList]
insert_in [lemma, in Sudoku.OrderedList]
invariant [definition, in Sudoku.Sudoku]
invariant_gen_init_clauses [lemma, in Sudoku.Sudoku]
invariant_equiv [lemma, in Sudoku.Sudoku]
invariant_init_c [lemma, in Sudoku.Sudoku]
invariant_refine [lemma, in Sudoku.Sudoku]
invariant_clauses_update1 [lemma, in Sudoku.Sudoku]
invariant_clauses_update [lemma, in Sudoku.Sudoku]
in_indexes [lemma, in Sudoku.Sudoku]
in_progression [lemma, in Sudoku.ListOp]
in_permutation_ex [lemma, in Sudoku.Permutation]
in_ex_app_first [lemma, in Sudoku.UList]
in_inv_dec [lemma, in Sudoku.UList]
in_fold_map [lemma, in Sudoku.ListAux]
In_dec1 [definition, in Sudoku.ListAux]
In_dec [definition, in Sudoku.ListAux]
in_list_prod_inv [lemma, in Sudoku.ListAux]
in_flat_map_ex [lemma, in Sudoku.ListAux]
in_flat_map [lemma, in Sudoku.ListAux]
in_map_fst_inv [lemma, in Sudoku.ListAux]
in_map_inv [lemma, in Sudoku.ListAux]
in_ex_nth [lemma, in Sudoku.ListAux]
in_ex_app [lemma, in Sudoku.ListAux]
is_in_correct [lemma, in Sudoku.OrderedList]
is_in [definition, in Sudoku.OrderedList]

J

jump [definition, in Sudoku.ListOp]
jump_add [lemma, in Sudoku.ListOp]
jump_too_far [lemma, in Sudoku.ListOp]
jump_nth [lemma, in Sudoku.ListOp]
jump_nil [lemma, in Sudoku.ListOp]

L

length_indexes [lemma, in Sudoku.Sudoku]
length_clauses_update [lemma, in Sudoku.Sudoku]
length_clauses_merge [lemma, in Sudoku.Sudoku]
length_clause_insert [lemma, in Sudoku.Sudoku]
length_rect [lemma, in Sudoku.Sudoku]
length_column [lemma, in Sudoku.Sudoku]
length_row [lemma, in Sudoku.Sudoku]
length_update [lemma, in Sudoku.Sudoku]
length_init [lemma, in Sudoku.Sudoku]
length_subst [lemma, in Sudoku.ListOp]
length_take_and_jump [lemma, in Sudoku.ListOp]
length_jump [lemma, in Sudoku.ListOp]
length_take1 [lemma, in Sudoku.ListOp]
length_take_small [lemma, in Sudoku.ListOp]
length_take [lemma, in Sudoku.ListOp]
length_list_prod [lemma, in Sudoku.ListAux]
length_map [lemma, in Sudoku.ListAux]
length_app [lemma, in Sudoku.ListAux]
lexico [definition, in Sudoku.OrderedList]
lexico_mult [lemma, in Sudoku.Div]
lexico_exact [lemma, in Sudoku.OrderedList]
lexico_anti_sym [lemma, in Sudoku.OrderedList]
lexico_trans [lemma, in Sudoku.OrderedList]
List [section, in Sudoku.ListAux]
ListAux [library]
ListOp [library]
list_op.o [variable, in Sudoku.ListOp]
list_op.A [variable, in Sudoku.ListOp]
list_op [section, in Sudoku.ListOp]
list_eq_dec [definition, in Sudoku.ListAux]
list_nth_eq [lemma, in Sudoku.ListAux]
list_length_induction [definition, in Sudoku.ListAux]
list_length_ind [lemma, in Sudoku.ListAux]
List.A [variable, in Sudoku.ListAux]
List.B [variable, in Sudoku.ListAux]
List.C [variable, in Sudoku.ListAux]
List.f [variable, in Sudoku.ListAux]
lit [inductive, in Sudoku.Sudoku]
lit_rm_sat [lemma, in Sudoku.Sudoku]
lit_sat [definition, in Sudoku.Sudoku]
lit_rm_valid [lemma, in Sudoku.Sudoku]
lit_insert_valid [lemma, in Sudoku.Sudoku]
lit_rm_in [lemma, in Sudoku.Sudoku]
lit_is_in_correct [lemma, in Sudoku.Sudoku]
lit_rm_ordered [lemma, in Sudoku.Sudoku]
lit_insert_ordered [lemma, in Sudoku.Sudoku]
lit_insert_in [lemma, in Sudoku.Sudoku]
lit_rm [definition, in Sudoku.Sudoku]
lit_insert [definition, in Sudoku.Sudoku]
lit_is_in [definition, in Sudoku.Sudoku]
lit_test_exact [lemma, in Sudoku.Sudoku]
lit_test_anti_sym [lemma, in Sudoku.Sudoku]
lit_test_trans [lemma, in Sudoku.Sudoku]
lit_test [definition, in Sudoku.Sudoku]
lt [constructor, in Sudoku.OrderedList]
l1 [definition, in Sudoku.Test]
l2 [definition, in Sudoku.Test]
l4 [definition, in Sudoku.Test]
l5 [definition, in Sudoku.Test]

M

map_length_decompose [lemma, in Sudoku.ListAux]
map_app [lemma, in Sudoku.ListAux]
merge [definition, in Sudoku.OrderedList]
merges [definition, in Sudoku.Sudoku]
merge_olist [lemma, in Sudoku.OrderedList]
merge_olist_strong [lemma, in Sudoku.OrderedList]
merge_inv [lemma, in Sudoku.OrderedList]
merge_incl_r [lemma, in Sudoku.OrderedList]
merge_incl_l [lemma, in Sudoku.OrderedList]
mk_0_length [lemma, in Sudoku.ListOp]
mk_0 [definition, in Sudoku.ListOp]
mod [definition, in Sudoku.Div]
mod_mult_comp [lemma, in Sudoku.Div]
mod_small [lemma, in Sudoku.Div]
mod_lt [lemma, in Sudoku.Div]
mod_aux_lt [lemma, in Sudoku.Div]
mod_aux [definition, in Sudoku.Div]
mult_lt_plus [lemma, in Sudoku.Div]

N

next [definition, in Sudoku.Sudoku]
next_pos [lemma, in Sudoku.Sudoku]
nth_ulist [lemma, in Sudoku.UList]
nth_default [lemma, in Sudoku.ListAux]
nth_app_r [lemma, in Sudoku.ListAux]
nth_app_l [lemma, in Sudoku.ListAux]
nth_nil [lemma, in Sudoku.ListAux]

O

ocons [definition, in Sudoku.OrderedList]
ocons_inv [lemma, in Sudoku.OrderedList]
ocons_incl [lemma, in Sudoku.OrderedList]
ocons_in [lemma, in Sudoku.OrderedList]
ocons_length [lemma, in Sudoku.OrderedList]
olist [inductive, in Sudoku.OrderedList]
olist_ulist [lemma, in Sudoku.OrderedList]
olist_weight [lemma, in Sudoku.OrderedList]
olist_skip [lemma, in Sudoku.OrderedList]
olist_inv [lemma, in Sudoku.OrderedList]
olist_cons [constructor, in Sudoku.OrderedList]
olist_one [constructor, in Sudoku.OrderedList]
olist_nil [constructor, in Sudoku.OrderedList]
opp [definition, in Sudoku.OrderedList]
ordered [definition, in Sudoku.Sudoku]
ordered [section, in Sudoku.OrderedList]
OrderedList [library]
ordered_clause [definition, in Sudoku.Sudoku]
ordered.A [variable, in Sudoku.OrderedList]
ordered.weight [variable, in Sudoku.OrderedList]
ordered.weight_exact [variable, in Sudoku.OrderedList]
ordered.weight_compat_l [variable, in Sudoku.OrderedList]
ordered.weight_anti_sym [variable, in Sudoku.OrderedList]
ordered.weight_trans [variable, in Sudoku.OrderedList]
out [definition, in Sudoku.Sudoku]
out_not_in_refl [lemma, in Sudoku.Sudoku]

P

permutation [inductive, in Sudoku.Permutation]
permutation [section, in Sudoku.Permutation]
Permutation [library]
permutation_flat_map [lemma, in Sudoku.Permutation]
permutation_map_ex [lemma, in Sudoku.Permutation]
permutation_map_ex_aux [variable, in Sudoku.Permutation]
permutation_map [lemma, in Sudoku.Permutation]
permutation_dec1 [definition, in Sudoku.Permutation]
permutation_dec [definition, in Sudoku.Permutation]
permutation_all_permutations [lemma, in Sudoku.Permutation]
permutation_inv [lemma, in Sudoku.Permutation]
permutation_cons_ex [lemma, in Sudoku.Permutation]
permutation_transposition [lemma, in Sudoku.Permutation]
permutation_app_swap [lemma, in Sudoku.Permutation]
permutation_app_comp [lemma, in Sudoku.Permutation]
permutation_in [lemma, in Sudoku.Permutation]
permutation_one_inv [lemma, in Sudoku.Permutation]
permutation_nil_inv [lemma, in Sudoku.Permutation]
permutation_length [lemma, in Sudoku.Permutation]
permutation_sym [lemma, in Sudoku.Permutation]
permutation_refl [lemma, in Sudoku.Permutation]
permutation_trans [constructor, in Sudoku.Permutation]
permutation_swap [constructor, in Sudoku.Permutation]
permutation_skip [constructor, in Sudoku.Permutation]
permutation_nil [constructor, in Sudoku.Permutation]
permutation.A [variable, in Sudoku.Permutation]
permutation.all_permutations_aux_permutation [variable, in Sudoku.Permutation]
permutation.permutation_all_permutations_aux [variable, in Sudoku.Permutation]
permutation.permutation_cons_ex_aux [variable, in Sudoku.Permutation]
permutation.permutation_one_inv_aux [variable, in Sudoku.Permutation]
Pos [constructor, in Sudoku.Sudoku]
pos [inductive, in Sudoku.Sudoku]
pos_dec [definition, in Sudoku.Sudoku]
pos_test_exact [lemma, in Sudoku.Sudoku]
pos_test_anti_sym [lemma, in Sudoku.Sudoku]
pos_test_trans [lemma, in Sudoku.Sudoku]
pos_test [definition, in Sudoku.Sudoku]
pos2n [definition, in Sudoku.Sudoku]
prestrict [definition, in Sudoku.Sudoku]
prestrict_get_default [lemma, in Sudoku.Sudoku]
prestrict_get [lemma, in Sudoku.Sudoku]
prestrict_update [lemma, in Sudoku.Sudoku]
prestrict_length [lemma, in Sudoku.Sudoku]
prestrict_all [lemma, in Sudoku.Sudoku]
prestrict_0 [lemma, in Sudoku.Sudoku]
progression [definition, in Sudoku.ListOp]
progression_list [lemma, in Sudoku.ListOp]

R

rect [definition, in Sudoku.Sudoku]
rect_aux2 [lemma, in Sudoku.Sudoku]
rect_aux1 [lemma, in Sudoku.Sudoku]
refine [definition, in Sudoku.Sudoku]
refine_update [lemma, in Sudoku.Sudoku]
refine_init [lemma, in Sudoku.Sudoku]
refine_trans [lemma, in Sudoku.Sudoku]
ref_list_length [lemma, in Sudoku.Sudoku]
ref_list_ulist [lemma, in Sudoku.Sudoku]
ref_list [definition, in Sudoku.Sudoku]
restrict [definition, in Sudoku.ListOp]
restrict_nth_default [lemma, in Sudoku.ListOp]
restrict_nth [lemma, in Sudoku.ListOp]
restrict_update [lemma, in Sudoku.ListOp]
restrict_length [lemma, in Sudoku.ListOp]
restrict_all [lemma, in Sudoku.ListOp]
restrict_0 [lemma, in Sudoku.ListOp]
rm [definition, in Sudoku.OrderedList]
rm_olist [lemma, in Sudoku.OrderedList]
rm_olist_strong [lemma, in Sudoku.OrderedList]
rm_in [lemma, in Sudoku.OrderedList]
rm_not_in [lemma, in Sudoku.OrderedList]
rm_incl [lemma, in Sudoku.OrderedList]
rm_cont [definition, in Sudoku.OrderedList]
row [definition, in Sudoku.Sudoku]

S

same_length_ex [lemma, in Sudoku.ListAux]
sat [definition, in Sudoku.Sudoku]
sat_refine [lemma, in Sudoku.Sudoku]
shift [definition, in Sudoku.Sudoku]
size [definition, in Sudoku.Sudoku]
split_one_in_ex [lemma, in Sudoku.Permutation]
split_one_permutation [lemma, in Sudoku.Permutation]
split_one [definition, in Sudoku.Permutation]
subst [definition, in Sudoku.ListOp]
sudoku [definition, in Sudoku.Sudoku]
Sudoku [library]
sudoku_refine_id [lemma, in Sudoku.Sudoku]

T

Tactic [library]
take [definition, in Sudoku.ListOp]
take_and_jump_nil [lemma, in Sudoku.ListOp]
take_and_jump [definition, in Sudoku.ListOp]
take_nth [lemma, in Sudoku.ListOp]
take_nil [lemma, in Sudoku.ListOp]
test [definition, in Sudoku.OrderedList]
Test [library]
test_compat_l [lemma, in Sudoku.OrderedList]
test_exact [lemma, in Sudoku.OrderedList]
test_anti_sym [lemma, in Sudoku.OrderedList]
test_trans [lemma, in Sudoku.OrderedList]
try_all_sat [lemma, in Sudoku.Sudoku]
try_all_olist [lemma, in Sudoku.Sudoku]
try_one_sat [lemma, in Sudoku.Sudoku]
try_all [definition, in Sudoku.Sudoku]
try_one [definition, in Sudoku.Sudoku]
t1 [definition, in Sudoku.Test]
t2 [definition, in Sudoku.Test]
t3 [definition, in Sudoku.Test]
t4 [definition, in Sudoku.Test]
t5 [definition, in Sudoku.Test]

U

ulist [inductive, in Sudoku.UList]
UList [library]
ulist_list_prod [lemma, in Sudoku.UList]
ulist_map [lemma, in Sudoku.UList]
ulist_inv_ulist [lemma, in Sudoku.UList]
ulist_incl_length_strict [lemma, in Sudoku.UList]
ulist_incl2_permutation [lemma, in Sudoku.UList]
ulist_incl_length [lemma, in Sudoku.UList]
ulist_eq_permutation [lemma, in Sudoku.UList]
ulist_incl_permutation [lemma, in Sudoku.UList]
ulist_def [lemma, in Sudoku.UList]
ulist_perm [lemma, in Sudoku.UList]
ulist_dec [definition, in Sudoku.UList]
ulist_app_inv_r [lemma, in Sudoku.UList]
ulist_app_inv_l [lemma, in Sudoku.UList]
ulist_app_inv [lemma, in Sudoku.UList]
ulist_app [lemma, in Sudoku.UList]
ulist_inv [lemma, in Sudoku.UList]
ulist_cons [constructor, in Sudoku.UList]
ulist_nil [constructor, in Sudoku.UList]
UniqueList [section, in Sudoku.UList]
UniqueList.A [variable, in Sudoku.UList]
UniqueList.eqA_dec [variable, in Sudoku.UList]
update [definition, in Sudoku.Sudoku]
update_diff_get [lemma, in Sudoku.Sudoku]
update_get [lemma, in Sudoku.Sudoku]

V

v [constructor, in Sudoku.Sudoku]
valid [definition, in Sudoku.Sudoku]
valid_init_c [lemma, in Sudoku.Sudoku]
valid_update [lemma, in Sudoku.Sudoku]
valid_refine [lemma, in Sudoku.Sudoku]
valid_lit_refine [lemma, in Sudoku.Sudoku]
valid_clause [definition, in Sudoku.Sudoku]
valid_lit [definition, in Sudoku.Sudoku]
valid_pos2n [lemma, in Sudoku.Sudoku]
valid_pos_next [lemma, in Sudoku.Sudoku]
valid_pos_eq [lemma, in Sudoku.Sudoku]
valid_pos [definition, in Sudoku.Sudoku]

W

weight_equiv [lemma, in Sudoku.OrderedList]
weight_compat_r [lemma, in Sudoku.OrderedList]
weight_refl [lemma, in Sudoku.OrderedList]
w_pos [lemma, in Sudoku.Sudoku]

Variable Index

C

check.h [in Sudoku.Sudoku]
check.w [in Sudoku.Sudoku]

L

list_op.o [in Sudoku.ListOp]
list_op.A [in Sudoku.ListOp]
List.A [in Sudoku.ListAux]
List.B [in Sudoku.ListAux]
List.C [in Sudoku.ListAux]
List.f [in Sudoku.ListAux]

O

ordered.A [in Sudoku.OrderedList]
ordered.weight [in Sudoku.OrderedList]
ordered.weight_exact [in Sudoku.OrderedList]
ordered.weight_compat_l [in Sudoku.OrderedList]
ordered.weight_anti_sym [in Sudoku.OrderedList]
ordered.weight_trans [in Sudoku.OrderedList]

P

permutation_map_ex_aux [in Sudoku.Permutation]
permutation.A [in Sudoku.Permutation]
permutation.all_permutations_aux_permutation [in Sudoku.Permutation]
permutation.permutation_all_permutations_aux [in Sudoku.Permutation]
permutation.permutation_cons_ex_aux [in Sudoku.Permutation]
permutation.permutation_one_inv_aux [in Sudoku.Permutation]

U

UniqueList.A [in Sudoku.UList]
UniqueList.eqA_dec [in Sudoku.UList]

Library Index

D

Div

L

O

P

S

Sudoku

T

U

UList

Lemma Index

A

add_inv [in Sudoku.OrderedList]
add_incl_r [in Sudoku.OrderedList]
add_incl_l [in Sudoku.OrderedList]
add_length [in Sudoku.OrderedList]
all_cell_sat [in Sudoku.Sudoku]
all_cell_ordered [in Sudoku.Sudoku]
all_permutations_permutation [in Sudoku.Permutation]
anti_literals_sat [in Sudoku.Sudoku]
anti_literals_in [in Sudoku.Sudoku]
anti_literals_ordered [in Sudoku.Sudoku]
app_inv_app2 [in Sudoku.ListAux]
app_inv_app [in Sudoku.ListAux]
app_inv_tail [in Sudoku.ListAux]
app_inv_head [in Sudoku.ListAux]

C

clauses_update_sat_rev [in Sudoku.Sudoku]
clauses_update_sat [in Sudoku.Sudoku]
clauses_merge_sat [in Sudoku.Sudoku]
clauses_update_valid [in Sudoku.Sudoku]
clauses_merge_valid [in Sudoku.Sudoku]
clauses_update_ordered [in Sudoku.Sudoku]
clauses_merge_in [in Sudoku.Sudoku]
clause_insert_sat [in Sudoku.Sudoku]
clause_insert_valid [in Sudoku.Sudoku]
clause_merge_valid [in Sudoku.Sudoku]
clause_insert_ordered [in Sudoku.Sudoku]
clause_merge_ordered [in Sudoku.Sudoku]
clause_insert_in [in Sudoku.Sudoku]
clause_merge_in [in Sudoku.Sudoku]
cross_correct [in Sudoku.Sudoku]
cross1_correct [in Sudoku.Sudoku]
cross2_correct [in Sudoku.Sudoku]

D

div_mult_comp [in Sudoku.Div]
div_is_0 [in Sudoku.Div]
div_lt [in Sudoku.Div]
div_mod_correct [in Sudoku.Div]
div_mod_aux_correct [in Sudoku.Div]

E

empty_take [in Sudoku.Sudoku]
empty_inv [in Sudoku.Sudoku]
empty_cons [in Sudoku.Sudoku]
empty_jump [in Sudoku.Sudoku]
empty_mk_0 [in Sudoku.Sudoku]
empty_nil [in Sudoku.Sudoku]

F

find_all_correct [in Sudoku.Sudoku]
find_one_correct [in Sudoku.Sudoku]
find_all_aux_sat [in Sudoku.Sudoku]
find_one_aux_sat [in Sudoku.Sudoku]
fold_clause_insert3 [in Sudoku.Sudoku]
fold_clause_insert2 [in Sudoku.Sudoku]
fold_clause_insert1 [in Sudoku.Sudoku]
fold_clause_insert_ordered [in Sudoku.Sudoku]
fold_insert2 [in Sudoku.Sudoku]
fold_insert1 [in Sudoku.Sudoku]

G

gen_cell_sat [in Sudoku.Sudoku]
gen_rect_sat [in Sudoku.Sudoku]
gen_column_sat [in Sudoku.Sudoku]
gen_row_sat [in Sudoku.Sudoku]
gen_init_clauses_valid [in Sudoku.Sudoku]
gen_init_clauses_ordered [in Sudoku.Sudoku]
gen_cell_ordered [in Sudoku.Sudoku]
gen_rect_ordered [in Sudoku.Sudoku]
gen_column_ordered [in Sudoku.Sudoku]
gen_row_ordered [in Sudoku.Sudoku]
gen_cell_correct [in Sudoku.Sudoku]
gen_rect_correct [in Sudoku.Sudoku]
gen_column_correct [in Sudoku.Sudoku]
gen_row_correct [in Sudoku.Sudoku]
get_rect [in Sudoku.Sudoku]
get_column [in Sudoku.Sudoku]
get_row [in Sudoku.Sudoku]
get_mk_0 [in Sudoku.Sudoku]
get_next [in Sudoku.Sudoku]
get_nil [in Sudoku.Sudoku]

H

h_pos [in Sudoku.Sudoku]

I

incl_length_repetition [in Sudoku.UList]
init_c_sudoku [in Sudoku.Sudoku]
init_c_sat [in Sudoku.Sudoku]
init_c_ordered [in Sudoku.Sudoku]
insert_olist [in Sudoku.OrderedList]
insert_inv [in Sudoku.OrderedList]
insert_incl [in Sudoku.OrderedList]
insert_in [in Sudoku.OrderedList]
invariant_gen_init_clauses [in Sudoku.Sudoku]
invariant_equiv [in Sudoku.Sudoku]
invariant_init_c [in Sudoku.Sudoku]
invariant_refine [in Sudoku.Sudoku]
invariant_clauses_update1 [in Sudoku.Sudoku]
invariant_clauses_update [in Sudoku.Sudoku]
in_indexes [in Sudoku.Sudoku]
in_progression [in Sudoku.ListOp]
in_permutation_ex [in Sudoku.Permutation]
in_ex_app_first [in Sudoku.UList]
in_inv_dec [in Sudoku.UList]
in_fold_map [in Sudoku.ListAux]
in_list_prod_inv [in Sudoku.ListAux]
in_flat_map_ex [in Sudoku.ListAux]
in_flat_map [in Sudoku.ListAux]
in_map_fst_inv [in Sudoku.ListAux]
in_map_inv [in Sudoku.ListAux]
in_ex_nth [in Sudoku.ListAux]
in_ex_app [in Sudoku.ListAux]
is_in_correct [in Sudoku.OrderedList]

J

jump_add [in Sudoku.ListOp]
jump_too_far [in Sudoku.ListOp]
jump_nth [in Sudoku.ListOp]
jump_nil [in Sudoku.ListOp]

L

length_indexes [in Sudoku.Sudoku]
length_clauses_update [in Sudoku.Sudoku]
length_clauses_merge [in Sudoku.Sudoku]
length_clause_insert [in Sudoku.Sudoku]
length_rect [in Sudoku.Sudoku]
length_column [in Sudoku.Sudoku]
length_row [in Sudoku.Sudoku]
length_update [in Sudoku.Sudoku]
length_init [in Sudoku.Sudoku]
length_subst [in Sudoku.ListOp]
length_take_and_jump [in Sudoku.ListOp]
length_jump [in Sudoku.ListOp]
length_take1 [in Sudoku.ListOp]
length_take_small [in Sudoku.ListOp]
length_take [in Sudoku.ListOp]
length_list_prod [in Sudoku.ListAux]
length_map [in Sudoku.ListAux]
length_app [in Sudoku.ListAux]
lexico_mult [in Sudoku.Div]
lexico_exact [in Sudoku.OrderedList]
lexico_anti_sym [in Sudoku.OrderedList]
lexico_trans [in Sudoku.OrderedList]
list_nth_eq [in Sudoku.ListAux]
list_length_ind [in Sudoku.ListAux]
lit_rm_sat [in Sudoku.Sudoku]
lit_rm_valid [in Sudoku.Sudoku]
lit_insert_valid [in Sudoku.Sudoku]
lit_rm_in [in Sudoku.Sudoku]
lit_is_in_correct [in Sudoku.Sudoku]
lit_rm_ordered [in Sudoku.Sudoku]
lit_insert_ordered [in Sudoku.Sudoku]
lit_insert_in [in Sudoku.Sudoku]
lit_test_exact [in Sudoku.Sudoku]
lit_test_anti_sym [in Sudoku.Sudoku]
lit_test_trans [in Sudoku.Sudoku]

M

map_length_decompose [in Sudoku.ListAux]
map_app [in Sudoku.ListAux]
merge_olist [in Sudoku.OrderedList]
merge_olist_strong [in Sudoku.OrderedList]
merge_inv [in Sudoku.OrderedList]
merge_incl_r [in Sudoku.OrderedList]
merge_incl_l [in Sudoku.OrderedList]
mk_0_length [in Sudoku.ListOp]
mod_mult_comp [in Sudoku.Div]
mod_small [in Sudoku.Div]
mod_lt [in Sudoku.Div]
mod_aux_lt [in Sudoku.Div]
mult_lt_plus [in Sudoku.Div]

N

next_pos [in Sudoku.Sudoku]
nth_ulist [in Sudoku.UList]
nth_default [in Sudoku.ListAux]
nth_app_r [in Sudoku.ListAux]
nth_app_l [in Sudoku.ListAux]
nth_nil [in Sudoku.ListAux]

O

ocons_inv [in Sudoku.OrderedList]
ocons_incl [in Sudoku.OrderedList]
ocons_in [in Sudoku.OrderedList]
ocons_length [in Sudoku.OrderedList]
olist_ulist [in Sudoku.OrderedList]
olist_weight [in Sudoku.OrderedList]
olist_skip [in Sudoku.OrderedList]
olist_inv [in Sudoku.OrderedList]
out_not_in_refl [in Sudoku.Sudoku]

P

permutation_flat_map [in Sudoku.Permutation]
permutation_map_ex [in Sudoku.Permutation]
permutation_map [in Sudoku.Permutation]
permutation_all_permutations [in Sudoku.Permutation]
permutation_inv [in Sudoku.Permutation]
permutation_cons_ex [in Sudoku.Permutation]
permutation_transposition [in Sudoku.Permutation]
permutation_app_swap [in Sudoku.Permutation]
permutation_app_comp [in Sudoku.Permutation]
permutation_in [in Sudoku.Permutation]
permutation_one_inv [in Sudoku.Permutation]
permutation_nil_inv [in Sudoku.Permutation]
permutation_length [in Sudoku.Permutation]
permutation_sym [in Sudoku.Permutation]
permutation_refl [in Sudoku.Permutation]
pos_test_exact [in Sudoku.Sudoku]
pos_test_anti_sym [in Sudoku.Sudoku]
pos_test_trans [in Sudoku.Sudoku]
prestrict_get_default [in Sudoku.Sudoku]
prestrict_get [in Sudoku.Sudoku]
prestrict_update [in Sudoku.Sudoku]
prestrict_length [in Sudoku.Sudoku]
prestrict_all [in Sudoku.Sudoku]
prestrict_0 [in Sudoku.Sudoku]
progression_list [in Sudoku.ListOp]

R

rect_aux2 [in Sudoku.Sudoku]
rect_aux1 [in Sudoku.Sudoku]
refine_update [in Sudoku.Sudoku]
refine_init [in Sudoku.Sudoku]
refine_trans [in Sudoku.Sudoku]
ref_list_length [in Sudoku.Sudoku]
ref_list_ulist [in Sudoku.Sudoku]
restrict_nth_default [in Sudoku.ListOp]
restrict_nth [in Sudoku.ListOp]
restrict_update [in Sudoku.ListOp]
restrict_length [in Sudoku.ListOp]
restrict_all [in Sudoku.ListOp]
restrict_0 [in Sudoku.ListOp]
rm_olist [in Sudoku.OrderedList]
rm_olist_strong [in Sudoku.OrderedList]
rm_in [in Sudoku.OrderedList]
rm_not_in [in Sudoku.OrderedList]
rm_incl [in Sudoku.OrderedList]

S

same_length_ex [in Sudoku.ListAux]
sat_refine [in Sudoku.Sudoku]
split_one_in_ex [in Sudoku.Permutation]
split_one_permutation [in Sudoku.Permutation]
sudoku_refine_id [in Sudoku.Sudoku]

T

take_and_jump_nil [in Sudoku.ListOp]
take_nth [in Sudoku.ListOp]
take_nil [in Sudoku.ListOp]
test_compat_l [in Sudoku.OrderedList]
test_exact [in Sudoku.OrderedList]
test_anti_sym [in Sudoku.OrderedList]
test_trans [in Sudoku.OrderedList]
try_all_sat [in Sudoku.Sudoku]
try_all_olist [in Sudoku.Sudoku]
try_one_sat [in Sudoku.Sudoku]

U

ulist_list_prod [in Sudoku.UList]
ulist_map [in Sudoku.UList]
ulist_inv_ulist [in Sudoku.UList]
ulist_incl_length_strict [in Sudoku.UList]
ulist_incl2_permutation [in Sudoku.UList]
ulist_incl_length [in Sudoku.UList]
ulist_eq_permutation [in Sudoku.UList]
ulist_incl_permutation [in Sudoku.UList]
ulist_def [in Sudoku.UList]
ulist_perm [in Sudoku.UList]
ulist_app_inv_r [in Sudoku.UList]
ulist_app_inv_l [in Sudoku.UList]
ulist_app_inv [in Sudoku.UList]
ulist_app [in Sudoku.UList]
ulist_inv [in Sudoku.UList]
update_diff_get [in Sudoku.Sudoku]
update_get [in Sudoku.Sudoku]

V

valid_init_c [in Sudoku.Sudoku]
valid_update [in Sudoku.Sudoku]
valid_refine [in Sudoku.Sudoku]
valid_lit_refine [in Sudoku.Sudoku]
valid_pos2n [in Sudoku.Sudoku]
valid_pos_next [in Sudoku.Sudoku]
valid_pos_eq [in Sudoku.Sudoku]

W

weight_equiv [in Sudoku.OrderedList]
weight_compat_r [in Sudoku.OrderedList]
weight_refl [in Sudoku.OrderedList]
w_pos [in Sudoku.Sudoku]

Constructor Index

E

eq [in Sudoku.OrderedList]

G

gt [in Sudoku.OrderedList]

L

lt [in Sudoku.OrderedList]

O

olist_cons [in Sudoku.OrderedList]
olist_one [in Sudoku.OrderedList]
olist_nil [in Sudoku.OrderedList]

P

permutation_trans [in Sudoku.Permutation]
permutation_swap [in Sudoku.Permutation]
permutation_skip [in Sudoku.Permutation]
permutation_nil [in Sudoku.Permutation]
Pos [in Sudoku.Sudoku]

U

ulist_cons [in Sudoku.UList]
ulist_nil [in Sudoku.UList]

V

v [in Sudoku.Sudoku]

Inductive Index

C

cmp [in Sudoku.OrderedList]

L

lit [in Sudoku.Sudoku]

O

olist [in Sudoku.OrderedList]

P

permutation [in Sudoku.Permutation]
pos [in Sudoku.Sudoku]

U

ulist [in Sudoku.UList]

Section Index

C

check [in Sudoku.Sudoku]

L

List [in Sudoku.ListAux]
list_op [in Sudoku.ListOp]

O

ordered [in Sudoku.OrderedList]

P

permutation [in Sudoku.Permutation]

U

UniqueList [in Sudoku.UList]

Definition Index

A

add [in Sudoku.OrderedList]
add_cont [in Sudoku.OrderedList]
all_cell [in Sudoku.Sudoku]
all_permutations [in Sudoku.Permutation]
all_permutations_aux [in Sudoku.Permutation]
anti_literals [in Sudoku.Sudoku]
A_dec [in Sudoku.OrderedList]

C

check [in Sudoku.Sudoku]
check_P [in Sudoku.Sudoku]
clause [in Sudoku.Sudoku]
clauses [in Sudoku.Sudoku]
clauses_update [in Sudoku.Sudoku]
clauses_merge [in Sudoku.Sudoku]
clause_sat [in Sudoku.Sudoku]
clause_insert [in Sudoku.Sudoku]
clause_merge [in Sudoku.Sudoku]
clause_test [in Sudoku.Sudoku]
column [in Sudoku.Sudoku]
cross [in Sudoku.Sudoku]
cross1 [in Sudoku.Sudoku]
cross2 [in Sudoku.Sudoku]

D

div [in Sudoku.Div]
div_aux [in Sudoku.Div]

E

empty [in Sudoku.Sudoku]
eq_nat [in Sudoku.OrderedList]

F

find_all [in Sudoku.Sudoku]
find_all_aux [in Sudoku.Sudoku]
find_one [in Sudoku.Sudoku]
find_one_aux [in Sudoku.Sudoku]

G

gen_init_clauses [in Sudoku.Sudoku]
gen_init_clauses_aux [in Sudoku.Sudoku]
gen_cell [in Sudoku.Sudoku]
gen_rect [in Sudoku.Sudoku]
gen_column [in Sudoku.Sudoku]
gen_row [in Sudoku.Sudoku]
get [in Sudoku.Sudoku]

I

indexes [in Sudoku.Sudoku]
init [in Sudoku.Sudoku]
init_c [in Sudoku.Sudoku]
insert [in Sudoku.OrderedList]
insert_cont [in Sudoku.OrderedList]
invariant [in Sudoku.Sudoku]
In_dec1 [in Sudoku.ListAux]
In_dec [in Sudoku.ListAux]
is_in [in Sudoku.OrderedList]

J

jump [in Sudoku.ListOp]

L

lexico [in Sudoku.OrderedList]
list_eq_dec [in Sudoku.ListAux]
list_length_induction [in Sudoku.ListAux]
lit_sat [in Sudoku.Sudoku]
lit_rm [in Sudoku.Sudoku]
lit_insert [in Sudoku.Sudoku]
lit_is_in [in Sudoku.Sudoku]
lit_test [in Sudoku.Sudoku]
l1 [in Sudoku.Test]
l2 [in Sudoku.Test]
l4 [in Sudoku.Test]
l5 [in Sudoku.Test]

M

merge [in Sudoku.OrderedList]
merges [in Sudoku.Sudoku]
mk_0 [in Sudoku.ListOp]
mod [in Sudoku.Div]
mod_aux [in Sudoku.Div]

N

next [in Sudoku.Sudoku]

O

ocons [in Sudoku.OrderedList]
opp [in Sudoku.OrderedList]
ordered [in Sudoku.Sudoku]
ordered_clause [in Sudoku.Sudoku]
out [in Sudoku.Sudoku]

P

permutation_dec1 [in Sudoku.Permutation]
permutation_dec [in Sudoku.Permutation]
pos_dec [in Sudoku.Sudoku]
pos_test [in Sudoku.Sudoku]
pos2n [in Sudoku.Sudoku]
prestrict [in Sudoku.Sudoku]
progression [in Sudoku.ListOp]

R

rect [in Sudoku.Sudoku]
refine [in Sudoku.Sudoku]
ref_list [in Sudoku.Sudoku]
restrict [in Sudoku.ListOp]
rm [in Sudoku.OrderedList]
rm_cont [in Sudoku.OrderedList]
row [in Sudoku.Sudoku]

S

sat [in Sudoku.Sudoku]
shift [in Sudoku.Sudoku]
size [in Sudoku.Sudoku]
split_one [in Sudoku.Permutation]
subst [in Sudoku.ListOp]
sudoku [in Sudoku.Sudoku]

T

take [in Sudoku.ListOp]
take_and_jump [in Sudoku.ListOp]
test [in Sudoku.OrderedList]
try_all [in Sudoku.Sudoku]
try_one [in Sudoku.Sudoku]
t1 [in Sudoku.Test]
t2 [in Sudoku.Test]
t3 [in Sudoku.Test]
t4 [in Sudoku.Test]
t5 [in Sudoku.Test]

U

ulist_dec [in Sudoku.UList]
update [in Sudoku.Sudoku]

V

valid [in Sudoku.Sudoku]
valid_clause [in Sudoku.Sudoku]
valid_lit [in Sudoku.Sudoku]
valid_pos [in Sudoku.Sudoku]

Global Index

B

K

Q

X

Y

Z

_

other

(416 entries)

Variable Index

A

B

D

E

F

G

H

I

J

K

M

N

Q

R

S

T

V

W

X

Y

Z

_

other

(22 entries)

Library Index

A

B

C

E

F

G

H

I

J

K

M

N

Q

R

V

W

X

Y

Z

_

other

(9 entries)

Lemma Index

B

K

Q

X

Y

Z

_

other

(254 entries)

Constructor Index

A

B

C

D

F

H

I

J

K

M

N

Q

R

S

T

W

X

Y

Z

_

other

(14 entries)

Inductive Index

A

B

D

E

F

G

H

I

J

K

M

N

Q

R

S

T

V

W

X

Y

Z

_

other

(6 entries)

Section Index

A

B

D

E

F

G

H

I

J

K

M

N

Q

R

S

T

V

W

X

Y

Z

_

other

(6 entries)

Definition Index

B

H

K

Q

W

X

Y

Z

_

other

(105 entries)