| 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 | (865 entries) |
| Notation 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 | (8 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 | _ | other | (4 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 | (20 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 | (40 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 | (396 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 | (8 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 | (4 entries) |
| Projection 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) |
| 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 | (60 entries) |
| Instance 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 | (60 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 | (259 entries) |
| Record 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) |
Global Index
A
abstr_not_pure [lemma, in exercises.pure]abstr_not_pure [lemma, in solutions.pure]
acquire [definition, in exercises.spin_lock]
acquire [definition, in solutions.spin_lock]
acquire [definition, in exercises.ticket_lock]
acquire [definition, in solutions.ticket_lock]
acquire_spec [lemma, in exercises.spin_lock]
acquire_spec [lemma, in solutions.spin_lock]
acquire_spec [lemma, in exercises.ticket_lock]
acquire_spec [lemma, in solutions.ticket_lock]
adequacy [library]
adequacy [library]
agree [section, in solutions.resource_algebra]
agree [section, in exercises.resource_algebra]
agree_valid_opL [lemma, in solutions.resource_algebra]
agree_dfrac_op [lemma, in solutions.resource_algebra]
agree_dfrac [lemma, in solutions.resource_algebra]
agree_core [lemma, in solutions.resource_algebra]
agree_valid [lemma, in solutions.resource_algebra]
agree_valid_opL [lemma, in exercises.resource_algebra]
agree_dfrac_op [lemma, in exercises.resource_algebra]
agree_dfrac [lemma, in exercises.resource_algebra]
agree_core [lemma, in exercises.resource_algebra]
agree_valid [lemma, in exercises.resource_algebra]
all [definition, in exercises.gr_predicates]
all [definition, in solutions.gr_predicates]
alloc [definition, in solutions.lang]
alloc [definition, in exercises.lang]
alloc_Start [lemma, in exercises.custom_ra]
alloc_Start [lemma, in solutions.custom_ra]
and_pure [lemma, in exercises.pure]
and_success [definition, in exercises.basics]
and_fail [definition, in exercises.basics]
and_pure [lemma, in solutions.pure]
and_success [definition, in solutions.basics]
and_fail [definition, in solutions.basics]
append [definition, in solutions.linked_lists]
append [definition, in exercises.linked_lists]
append_spec [lemma, in solutions.linked_lists]
append_spec [lemma, in exercises.linked_lists]
arith [definition, in solutions.lang]
arith [definition, in exercises.specifications]
arith [definition, in exercises.lang]
arith [definition, in solutions.specifications]
arith_spec [lemma, in exercises.specifications]
arith_spec [lemma, in solutions.specifications]
arrays [library]
arrays [library]
asdfd [lemma, in exercises.basics]
asm [lemma, in exercises.basics]
asm [lemma, in solutions.basics]
asmb [lemma, in exercises.basics]
asm_pure [lemma, in exercises.pure]
asm_pure [lemma, in solutions.pure]
B
basics [library]basics [library]
body_spec [lemma, in exercises.custom_ra]
body_spec [lemma, in solutions.custom_ra]
booleans [definition, in solutions.lang]
booleans [definition, in exercises.lang]
C
cas [definition, in solutions.lang]cas [definition, in exercises.specifications]
cas [definition, in exercises.lang]
cas [definition, in solutions.specifications]
cas_spec [lemma, in exercises.specifications]
cas_spec [lemma, in solutions.specifications]
cfg [definition, in solutions.adequacy]
cfg [definition, in exercises.adequacy]
cmpxchg_suc [definition, in solutions.lang]
cmpxchg_fail [definition, in solutions.lang]
cmpXchg_0_to_10_spec [lemma, in exercises.specifications]
cmpXchg_0_to_10 [definition, in exercises.specifications]
cmpxchg_suc [definition, in exercises.lang]
cmpxchg_fail [definition, in exercises.lang]
cmpXchg_0_to_10_spec [lemma, in solutions.specifications]
cmpXchg_0_to_10 [definition, in solutions.specifications]
copy [definition, in solutions.arrays]
copy [definition, in exercises.arrays]
copy_spec [lemma, in solutions.arrays]
copy_to_spec [lemma, in solutions.arrays]
copy_to [definition, in solutions.arrays]
copy_spec [lemma, in exercises.arrays]
copy_to_spec [lemma, in exercises.arrays]
copy_to [definition, in exercises.arrays]
count [definition, in solutions.later]
count [definition, in exercises.later]
counter [definition, in exercises.persistently]
counter [definition, in solutions.persistently]
counter [library]
counter [library]
counter_spec [lemma, in exercises.persistently]
counter_spec [lemma, in solutions.persistently]
count_spec [lemma, in solutions.later]
count_spec [lemma, in exercises.later]
custom_ra [library]
custom_ra [library]
D
dfrac_alloc_one [lemma, in solutions.resource_algebra]dfrac_update_own_both [lemma, in solutions.resource_algebra]
dfrac_update_own_own [lemma, in solutions.resource_algebra]
dfrac_update_ident [lemma, in solutions.resource_algebra]
dfrac_update_disc [definition, in solutions.resource_algebra]
dfrac_update [definition, in solutions.resource_algebra]
dfrac_pre_own_both [lemma, in solutions.resource_algebra]
dfrac_pre_disc_both [lemma, in solutions.resource_algebra]
dfrac_pre_own [lemma, in solutions.resource_algebra]
dfrac_core_both [lemma, in solutions.resource_algebra]
dfrac_core_discarded [lemma, in solutions.resource_algebra]
dfrac_core_own [lemma, in solutions.resource_algebra]
dfrac_invalid_own [lemma, in solutions.resource_algebra]
dfrac_valid_discarded [lemma, in solutions.resource_algebra]
dfrac_valid_own [lemma, in solutions.resource_algebra]
dfrac_op_comm [lemma, in solutions.resource_algebra]
dfrac_op_assoc [lemma, in solutions.resource_algebra]
dfrac_op_frac_both [lemma, in solutions.resource_algebra]
dfrac_op_both_disc [lemma, in solutions.resource_algebra]
dfrac_op_both [lemma, in solutions.resource_algebra]
dfrac_op_disc [lemma, in solutions.resource_algebra]
dfrac_op2 [lemma, in solutions.resource_algebra]
dfrac_op [lemma, in solutions.resource_algebra]
dfrac_frac_equiv [lemma, in solutions.resource_algebra]
dfrac_equiv_leibniz [lemma, in solutions.resource_algebra]
dfrac_alloc_one [lemma, in exercises.resource_algebra]
dfrac_update_own_both [lemma, in exercises.resource_algebra]
dfrac_update_own_own [lemma, in exercises.resource_algebra]
dfrac_update_ident [lemma, in exercises.resource_algebra]
dfrac_update_disc [definition, in exercises.resource_algebra]
dfrac_update [definition, in exercises.resource_algebra]
dfrac_pre_own_both [lemma, in exercises.resource_algebra]
dfrac_pre_disc_both [lemma, in exercises.resource_algebra]
dfrac_pre_own [lemma, in exercises.resource_algebra]
dfrac_core_both [lemma, in exercises.resource_algebra]
dfrac_core_discarded [lemma, in exercises.resource_algebra]
dfrac_core_own [lemma, in exercises.resource_algebra]
dfrac_invalid_own [lemma, in exercises.resource_algebra]
dfrac_valid_discarded [lemma, in exercises.resource_algebra]
dfrac_valid_own [lemma, in exercises.resource_algebra]
dfrac_op_comm [lemma, in exercises.resource_algebra]
dfrac_op_assoc [lemma, in exercises.resource_algebra]
dfrac_op_frac_both [lemma, in exercises.resource_algebra]
dfrac_op_both_disc [lemma, in exercises.resource_algebra]
dfrac_op_both [lemma, in exercises.resource_algebra]
dfrac_op_disc [lemma, in exercises.resource_algebra]
dfrac_op2 [lemma, in exercises.resource_algebra]
dfrac_op [lemma, in exercises.resource_algebra]
dfrac_frac_equiv [lemma, in exercises.resource_algebra]
dfrac_equiv_leibniz [lemma, in exercises.resource_algebra]
disagree_dfrac [lemma, in solutions.resource_algebra]
disagree_dfrac [lemma, in exercises.resource_algebra]
E
eq_elm [lemma, in exercises.pure]eq_5_5 [lemma, in exercises.pure]
eq_elm [lemma, in solutions.pure]
eq_5_5 [lemma, in solutions.pure]
exclusive [section, in solutions.resource_algebra]
exclusive [section, in exercises.resource_algebra]
excl_op_dfrac [definition, in solutions.resource_algebra]
excl_op [lemma, in solutions.resource_algebra]
excl_bot_invalid [lemma, in solutions.resource_algebra]
excl_valid [lemma, in solutions.resource_algebra]
excl_core [lemma, in solutions.resource_algebra]
excl_op_dfrac [definition, in exercises.resource_algebra]
excl_op [lemma, in exercises.resource_algebra]
excl_bot_invalid [lemma, in exercises.resource_algebra]
excl_valid [lemma, in exercises.resource_algebra]
excl_core [lemma, in exercises.resource_algebra]
F
Final [constructor, in exercises.custom_ra]Final [constructor, in solutions.custom_ra]
Final_core_id [instance, in exercises.custom_ra]
Final_core_id [instance, in solutions.custom_ra]
first_is_5 [lemma, in exercises.persistently]
first_is_5 [lemma, in exercises.persistently]
first_is_5 [lemma, in solutions.persistently]
first_is_5 [lemma, in solutions.persistently]
fold_right_spec [lemma, in solutions.linked_lists]
fold_right [definition, in solutions.linked_lists]
fold_right_spec [lemma, in exercises.linked_lists]
fold_right [definition, in exercises.linked_lists]
fork [definition, in solutions.lang]
fork [definition, in exercises.lang]
fun2stream [definition, in exercises.ofe]
fun2stream [definition, in solutions.ofe]
fun2stream_nth [lemma, in exercises.ofe]
fun2stream_nth [lemma, in solutions.ofe]
G
ghost [section, in solutions.resource_algebra]ghost [section, in exercises.resource_algebra]
gr_predicates [library]
gr_predicates [library]
H
handle_inv [definition, in exercises.structured_conc]handle_inv1 [definition, in exercises.structured_conc]
handle_inv [definition, in solutions.structured_conc]
handle_inv1 [definition, in solutions.structured_conc]
head [projection, in exercises.ofe]
head [projection, in solutions.ofe]
heaplang [section, in solutions.lang]
heaplang [section, in exercises.lang]
hoare_triple_dfrac [lemma, in solutions.resource_algebra]
hoare_triple_dfrac [lemma, in exercises.resource_algebra]
I
if_then_else [definition, in solutions.lang]if_then_else [definition, in exercises.lang]
inc [definition, in solutions.arrays]
inc [definition, in solutions.linked_lists]
inc [definition, in exercises.linked_lists]
inc [definition, in exercises.arrays]
incr [definition, in exercises.counter]
incr [definition, in solutions.counter]
inc_spec [lemma, in solutions.arrays]
inc_spec [lemma, in solutions.linked_lists]
inc_spec [lemma, in exercises.linked_lists]
inc_spec [lemma, in exercises.arrays]
Invalid [constructor, in exercises.custom_ra]
Invalid [constructor, in solutions.custom_ra]
invariants [library]
invariants [library]
inv_alloc_loc [lemma, in exercises.invariants]
inv_open_example [lemma, in exercises.invariants]
inv_open_example_attempt_2 [lemma, in exercises.invariants]
inv_open_example_attempt_1 [lemma, in exercises.invariants]
inv_open_fail [lemma, in exercises.invariants]
inv_persist [lemma, in exercises.invariants]
inv_timeless' [lemma, in solutions.timeless]
inv_timeless [lemma, in solutions.timeless]
inv_alloc_loc [lemma, in solutions.invariants]
inv_open_example [lemma, in solutions.invariants]
inv_open_example_attempt_2 [lemma, in solutions.invariants]
inv_open_example_attempt_1 [lemma, in solutions.invariants]
inv_open_fail [lemma, in solutions.invariants]
inv_persist [lemma, in solutions.invariants]
inv_timeless' [lemma, in exercises.timeless]
inv_timeless [lemma, in exercises.timeless]
isList [definition, in solutions.linked_lists]
isList [definition, in exercises.linked_lists]
issued [definition, in exercises.ticket_lock]
issued [definition, in solutions.ticket_lock]
is_lock [definition, in exercises.spin_lock]
is_lock [definition, in solutions.spin_lock]
is_lock [definition, in exercises.ticket_lock]
is_lock [definition, in solutions.ticket_lock]
is_list_rec_correct [lemma, in exercises.gr_predicates]
is_list_rec_ind [lemma, in exercises.gr_predicates]
is_list_rec_unfold [lemma, in exercises.gr_predicates]
is_list_rec [definition, in exercises.gr_predicates]
is_list_pre_mono [instance, in exercises.gr_predicates]
is_list_pre [definition, in exercises.gr_predicates]
is_list [definition, in exercises.gr_predicates]
is_list_of [definition, in exercises.gr_predicates]
is_list_rec_correct [lemma, in solutions.gr_predicates]
is_list_rec_ind [lemma, in solutions.gr_predicates]
is_list_rec_unfold [lemma, in solutions.gr_predicates]
is_list_rec [definition, in solutions.gr_predicates]
is_list_pre_mono [instance, in solutions.gr_predicates]
is_list_pre [definition, in solutions.gr_predicates]
is_list [definition, in solutions.gr_predicates]
is_list_of [definition, in solutions.gr_predicates]
J
join [definition, in exercises.structured_conc]join [definition, in solutions.structured_conc]
join_spec [lemma, in exercises.structured_conc]
join_handle [definition, in exercises.structured_conc]
join_spec [lemma, in exercises.structured_conc]
join_handle1 [definition, in exercises.structured_conc]
join_spec [lemma, in solutions.structured_conc]
join_handle [definition, in solutions.structured_conc]
join_spec [lemma, in solutions.structured_conc]
join_handle1 [definition, in solutions.structured_conc]
L
lambda [definition, in solutions.lang]lambda [definition, in exercises.specifications]
lambda [definition, in exercises.lang]
lambda [definition, in solutions.specifications]
lambda_spec [lemma, in exercises.specifications]
lambda_spec [lemma, in solutions.specifications]
lang [library]
lang [library]
later [section, in solutions.later]
later [section, in exercises.later]
later [library]
later [library]
later_timeless_strip [lemma, in solutions.timeless]
later_store' [lemma, in solutions.timeless]
later_store [lemma, in solutions.timeless]
later_timeless_fup' [lemma, in solutions.timeless]
later_timeless_fup [lemma, in solutions.timeless]
later_points_to [lemma, in solutions.later]
later_impl [lemma, in solutions.later]
later_sep [lemma, in solutions.later]
later_weak [lemma, in solutions.later]
later_mono' [lemma, in solutions.later]
later_mono [lemma, in solutions.later]
later_points_to [lemma, in exercises.later]
later_impl [lemma, in exercises.later]
later_sep [lemma, in exercises.later]
later_weak [lemma, in exercises.later]
later_mono' [lemma, in exercises.later]
later_mono [lemma, in exercises.later]
later_timeless_strip [lemma, in exercises.timeless]
later_store' [lemma, in exercises.timeless]
later_store [lemma, in exercises.timeless]
later_timeless_fup' [lemma, in exercises.timeless]
later_timeless_fup [lemma, in exercises.timeless]
lets [definition, in solutions.lang]
lets [definition, in exercises.lang]
linked_lists [section, in solutions.linked_lists]
linked_lists [section, in exercises.linked_lists]
linked_lists [library]
linked_lists [library]
load [definition, in solutions.lang]
load [definition, in exercises.lang]
locked [definition, in exercises.spin_lock]
locked [definition, in solutions.spin_lock]
locked [definition, in exercises.ticket_lock]
locked [definition, in solutions.ticket_lock]
locked_excl [lemma, in exercises.spin_lock]
locked_alloc [lemma, in exercises.spin_lock]
locked_excl [lemma, in solutions.spin_lock]
locked_alloc [lemma, in solutions.spin_lock]
locked_excl [lemma, in exercises.ticket_lock]
locked_by [definition, in exercises.ticket_lock]
locked_excl [lemma, in solutions.ticket_lock]
locked_by [definition, in solutions.ticket_lock]
lock_inv [definition, in exercises.spin_lock]
lock_inv [definition, in solutions.spin_lock]
lock_inv [definition, in exercises.ticket_lock]
lock_inv [definition, in solutions.ticket_lock]
M
merge [definition, in solutions.merge_sort]merge [definition, in exercises.merge_sort]
merge_sort_spec [lemma, in solutions.merge_sort]
merge_sort_inner_spec [lemma, in solutions.merge_sort]
merge_spec [lemma, in solutions.merge_sort]
merge_sort [definition, in solutions.merge_sort]
merge_sort_inner [definition, in solutions.merge_sort]
merge_sort_spec [lemma, in exercises.merge_sort]
merge_sort_inner_spec [lemma, in exercises.merge_sort]
merge_spec [lemma, in exercises.merge_sort]
merge_sort [definition, in exercises.merge_sort]
merge_sort_inner [definition, in exercises.merge_sort]
merge_sort [library]
merge_sort [library]
mk_counter [definition, in exercises.counter]
mk_lock_spec [lemma, in exercises.spin_lock]
mk_lock [definition, in exercises.spin_lock]
mk_lock_spec [lemma, in solutions.spin_lock]
mk_lock [definition, in solutions.spin_lock]
mk_lock_spec [lemma, in exercises.ticket_lock]
mk_lock [definition, in exercises.ticket_lock]
mk_lock_spec [lemma, in solutions.ticket_lock]
mk_lock [definition, in solutions.ticket_lock]
mk_counter [definition, in solutions.counter]
modus_ponens [lemma, in exercises.basics]
modus_ponens [lemma, in solutions.basics]
myPredFix [definition, in exercises.persistently]
myPredFix [definition, in solutions.persistently]
myPredFix_persistent [instance, in exercises.persistently]
myPredFix_persistent [instance, in solutions.persistently]
myPredicate [definition, in exercises.persistently]
myPredicate [definition, in solutions.persistently]
myPredicate_persistent' [instance, in exercises.persistently]
myPredicate_persistent [instance, in exercises.persistently]
myPredicate_persistent' [instance, in solutions.persistently]
myPredicate_persistent [instance, in solutions.persistently]
N
not_in_pers_context [lemma, in exercises.persistently]not_stuck [definition, in solutions.adequacy]
not_in_pers_context [lemma, in solutions.persistently]
not_stuck [definition, in exercises.adequacy]
nth [definition, in exercises.ofe]
nth [definition, in solutions.ofe]
nth_proper [instance, in exercises.ofe]
nth_proper [instance, in solutions.ofe]
O
ofe [section, in exercises.ofe]ofe [section, in solutions.ofe]
ofe [library]
ofe [library]
only_read [lemma, in exercises.persistently]
only_read [lemma, in solutions.persistently]
option [definition, in solutions.lang]
option [definition, in exercises.lang]
or_elim [lemma, in exercises.basics]
or_comm [lemma, in exercises.basics]
or_elim [lemma, in solutions.basics]
or_comm [lemma, in solutions.basics]
own_dfrac_update [lemma, in solutions.resource_algebra]
own_dfrac_both_disc [lemma, in solutions.resource_algebra]
own_dfrac_disc_persistent [lemma, in solutions.resource_algebra]
own_token_exclusive' [lemma, in solutions.resource_algebra]
own_token_exclusive [lemma, in solutions.resource_algebra]
own_op_dfrac [lemma, in solutions.resource_algebra]
own_dfrac_update [lemma, in exercises.resource_algebra]
own_dfrac_both_disc [lemma, in exercises.resource_algebra]
own_dfrac_disc_persistent [lemma, in exercises.resource_algebra]
own_token_exclusive' [lemma, in exercises.resource_algebra]
own_token_exclusive [lemma, in exercises.resource_algebra]
own_op_dfrac [lemma, in exercises.resource_algebra]
P
pairs [definition, in solutions.lang]pairs [definition, in exercises.lang]
pair_pcore_dfrac [lemma, in solutions.resource_algebra]
pair_pcore_some [lemma, in solutions.resource_algebra]
pair_pcore_dfrac [lemma, in exercises.resource_algebra]
pair_pcore_some [lemma, in exercises.resource_algebra]
par [definition, in solutions.lang]
par [definition, in exercises.lang]
par [section, in exercises.structured_conc]
par [definition, in exercises.structured_conc]
par [section, in solutions.structured_conc]
par [definition, in solutions.structured_conc]
parallel_add_spec [lemma, in exercises.structured_conc]
parallel_add_inv [definition, in exercises.structured_conc]
parallel_add.N [variable, in exercises.structured_conc]
parallel_add [section, in exercises.structured_conc]
parallel_add [definition, in exercises.structured_conc]
parallel_add_spec [lemma, in solutions.structured_conc]
parallel_add_inv [definition, in solutions.structured_conc]
parallel_add.N [variable, in solutions.structured_conc]
parallel_add [section, in solutions.structured_conc]
parallel_add [definition, in solutions.structured_conc]
par_read_spec [lemma, in exercises.persistently]
par_read [definition, in exercises.persistently]
par_read_write_spec [lemma, in exercises.persistently]
par_read_write [definition, in exercises.persistently]
par_client_spec [lemma, in exercises.specifications]
par_client [definition, in exercises.specifications]
par_client_spec [lemma, in solutions.specifications]
par_client [definition, in solutions.specifications]
par_read_spec [lemma, in solutions.persistently]
par_read [definition, in solutions.persistently]
par_read_write_spec [lemma, in solutions.persistently]
par_read_write [definition, in solutions.persistently]
par_spec [lemma, in exercises.structured_conc]
par_spec [lemma, in solutions.structured_conc]
persistently [section, in exercises.persistently]
persistently [section, in solutions.persistently]
persistently [library]
persistently [library]
pers_all [lemma, in exercises.persistently]
pers_sep [lemma, in exercises.persistently]
pers_idemp [lemma, in exercises.persistently]
pers_intro [lemma, in exercises.persistently]
pers_dup [lemma, in exercises.persistently]
pers_context [lemma, in exercises.persistently]
pers_all [lemma, in solutions.persistently]
pers_sep [lemma, in solutions.persistently]
pers_idemp [lemma, in solutions.persistently]
pers_intro [lemma, in solutions.persistently]
pers_dup [lemma, in solutions.persistently]
pers_context [lemma, in solutions.persistently]
power2 [definition, in exercises.ofe]
power2 [definition, in exercises.ofe]
power2 [definition, in solutions.ofe]
power2 [definition, in solutions.ofe]
power2_alt_correct [lemma, in exercises.ofe]
power2_alt_unfold [lemma, in exercises.ofe]
power2_alt [definition, in exercises.ofe]
power2_pre_contractive [instance, in exercises.ofe]
power2_pre [definition, in exercises.ofe]
power2_unfold [lemma, in exercises.ofe]
power2_helper_unfold [lemma, in exercises.ofe]
power2_helper [definition, in exercises.ofe]
power2_alt_correct [lemma, in solutions.ofe]
power2_alt_unfold [lemma, in solutions.ofe]
power2_alt [definition, in solutions.ofe]
power2_pre_contractive [instance, in solutions.ofe]
power2_pre [definition, in solutions.ofe]
power2_unfold [lemma, in solutions.ofe]
power2_helper_unfold [lemma, in solutions.ofe]
power2_helper [definition, in solutions.ofe]
product [section, in solutions.resource_algebra]
product [section, in exercises.resource_algebra]
prog [definition, in exercises.invariants]
prog [definition, in exercises.spin_lock]
prog [definition, in exercises.specifications]
prog [definition, in solutions.spin_lock]
prog [definition, in solutions.specifications]
prog [definition, in exercises.custom_ra]
prog [definition, in solutions.invariants]
prog [definition, in solutions.custom_ra]
prog_inv [definition, in exercises.invariants]
prog_spec [lemma, in exercises.spin_lock]
prog_adequacy [lemma, in solutions.adequacy]
prog_add_2_spec'' [lemma, in exercises.specifications]
prog_add_2_spec' [lemma, in exercises.specifications]
prog_spec_2 [lemma, in exercises.specifications]
prog_add_2_spec [lemma, in exercises.specifications]
prog_spec [lemma, in exercises.specifications]
prog_spec [lemma, in solutions.spin_lock]
prog_add_2_spec'' [lemma, in solutions.specifications]
prog_add_2_spec' [lemma, in solutions.specifications]
prog_spec_2 [lemma, in solutions.specifications]
prog_add_2_spec [lemma, in solutions.specifications]
prog_spec [lemma, in solutions.specifications]
prog_spec [lemma, in exercises.custom_ra]
prog_inv [definition, in solutions.invariants]
prog_adequacy [lemma, in exercises.adequacy]
prog_spec [lemma, in solutions.custom_ra]
prog2 [definition, in exercises.invariants]
prog2 [definition, in solutions.invariants]
prog2_spec [lemma, in exercises.invariants]
prog2_inv [definition, in exercises.invariants]
prog2_spec [lemma, in solutions.invariants]
prog2_inv [definition, in solutions.invariants]
progΣ [definition, in solutions.adequacy]
progΣ [definition, in exercises.adequacy]
proofs [section, in exercises.invariants]
proofs [section, in exercises.invariants]
proofs [section, in exercises.spin_lock]
proofs [section, in exercises.pure]
proofs [section, in solutions.spin_lock]
proofs [section, in exercises.ticket_lock]
proofs [section, in solutions.arrays]
proofs [section, in solutions.ticket_lock]
proofs [section, in exercises.gr_predicates]
proofs [section, in solutions.merge_sort]
proofs [section, in exercises.custom_ra]
proofs [section, in solutions.invariants]
proofs [section, in solutions.invariants]
proofs [section, in solutions.gr_predicates]
proofs [section, in exercises.merge_sort]
proofs [section, in exercises.basics]
proofs [section, in solutions.custom_ra]
proofs [section, in solutions.pure]
proofs [section, in solutions.basics]
proofs [section, in exercises.arrays]
proofs.inv_intro.N [variable, in exercises.invariants]
proofs.inv_intro [section, in exercises.invariants]
proofs.inv_intro.N [variable, in solutions.invariants]
proofs.inv_intro [section, in solutions.invariants]
proofs.N [variable, in exercises.invariants]
proofs.N [variable, in exercises.invariants]
proofs.N [variable, in exercises.spin_lock]
proofs.N [variable, in solutions.spin_lock]
proofs.N [variable, in exercises.ticket_lock]
proofs.N [variable, in solutions.ticket_lock]
proofs.N [variable, in exercises.custom_ra]
proofs.N [variable, in solutions.invariants]
proofs.N [variable, in solutions.invariants]
proofs.N [variable, in solutions.custom_ra]
_ ⊢ _ [notation, in exercises.pure]
_ ⊢ _ [notation, in solutions.pure]
⊢ _ [notation, in exercises.pure]
⊢ _ [notation, in solutions.pure]
properties [section, in exercises.custom_ra]
properties [section, in solutions.custom_ra]
pt_persist [lemma, in exercises.persistently]
pt_split [lemma, in exercises.persistently]
pt_not_dupl [lemma, in exercises.specifications]
pt_not_dupl [lemma, in solutions.specifications]
pt_persist [lemma, in solutions.persistently]
pt_split [lemma, in solutions.persistently]
pure [library]
pure [library]
pure_adj2 [lemma, in exercises.pure]
pure_adj1 [lemma, in exercises.pure]
pure_adj2 [lemma, in solutions.pure]
pure_adj1 [lemma, in solutions.pure]
R
RA [definition, in exercises.ticket_lock]RA [definition, in solutions.ticket_lock]
race [definition, in exercises.specifications]
race [definition, in solutions.specifications]
race_spec [definition, in solutions.specifications]
read [definition, in exercises.counter]
read [definition, in solutions.counter]
recursion [definition, in solutions.lang]
recursion [definition, in exercises.lang]
release [definition, in exercises.spin_lock]
release [definition, in solutions.spin_lock]
release [definition, in exercises.ticket_lock]
release [definition, in solutions.ticket_lock]
release_spec [lemma, in exercises.spin_lock]
release_spec [lemma, in solutions.spin_lock]
release_spec [lemma, in exercises.ticket_lock]
release_spec [lemma, in solutions.ticket_lock]
repeat [definition, in exercises.ofe]
repeat [definition, in solutions.ofe]
repeat_with_sep_alt_correct [lemma, in exercises.ofe]
repeat_with_sep_alt_unfold [lemma, in exercises.ofe]
repeat_with_sep_alt [definition, in exercises.ofe]
repeat_with_sep_contractive [instance, in exercises.ofe]
repeat_with_sep_pre [definition, in exercises.ofe]
repeat_with_sep_unfold [lemma, in exercises.ofe]
repeat_with_sep_helper_unfold [lemma, in exercises.ofe]
repeat_with_sep [definition, in exercises.ofe]
repeat_with_sep_helper [definition, in exercises.ofe]
repeat_with_sep [definition, in exercises.ofe]
repeat_with_sep_alt_correct [lemma, in solutions.ofe]
repeat_with_sep_alt_unfold [lemma, in solutions.ofe]
repeat_with_sep_alt [definition, in solutions.ofe]
repeat_with_sep_contractive [instance, in solutions.ofe]
repeat_with_sep_pre [definition, in solutions.ofe]
repeat_with_sep_unfold [lemma, in solutions.ofe]
repeat_with_sep_helper_unfold [lemma, in solutions.ofe]
repeat_with_sep [definition, in solutions.ofe]
repeat_with_sep_helper [definition, in solutions.ofe]
repeat_with_sep [definition, in solutions.ofe]
resource_algebra [library]
resource_algebra [library]
reverse [definition, in solutions.arrays]
reverse [definition, in solutions.linked_lists]
reverse [definition, in exercises.linked_lists]
reverse [definition, in exercises.arrays]
reverse_spec [lemma, in solutions.arrays]
reverse_spec [lemma, in solutions.linked_lists]
reverse_append_spec [lemma, in solutions.linked_lists]
reverse_append [definition, in solutions.linked_lists]
reverse_spec [lemma, in exercises.linked_lists]
reverse_append_spec [lemma, in exercises.linked_lists]
reverse_append [definition, in exercises.linked_lists]
reverse_spec [lemma, in exercises.arrays]
S
sapp [definition, in exercises.ofe]sapp [definition, in solutions.ofe]
sapp_proper [instance, in exercises.ofe]
sapp_ne [instance, in exercises.ofe]
sapp_proper [instance, in solutions.ofe]
sapp_ne [instance, in solutions.ofe]
SCons_proper [instance, in exercises.ofe]
SCons_ne [instance, in exercises.ofe]
SCons_contractive [instance, in exercises.ofe]
SCons_proper [instance, in solutions.ofe]
SCons_ne [instance, in solutions.ofe]
SCons_contractive [instance, in solutions.ofe]
sep_pure [lemma, in exercises.pure]
sep_all_distr [lemma, in exercises.basics]
sep_ex_distr [lemma, in exercises.basics]
sep_or_distr [lemma, in exercises.basics]
sep_comm_v2 [lemma, in exercises.basics]
sep_assoc_1 [lemma, in exercises.basics]
sep_comm [lemma, in exercises.basics]
sep_pure [lemma, in solutions.pure]
sep_all_distr [lemma, in solutions.basics]
sep_ex_distr [lemma, in solutions.basics]
sep_or_distr [lemma, in solutions.basics]
sep_comm_v2 [lemma, in solutions.basics]
sep_assoc_1 [lemma, in solutions.basics]
sep_comm [lemma, in solutions.basics]
spawn [definition, in solutions.lang]
spawn [definition, in exercises.lang]
spawn [section, in exercises.structured_conc]
spawn [definition, in exercises.structured_conc]
spawn [section, in solutions.structured_conc]
spawn [definition, in solutions.structured_conc]
spawn_spec [lemma, in exercises.structured_conc]
spawn_spec [lemma, in solutions.structured_conc]
spawn.N [variable, in exercises.structured_conc]
spawn.N [variable, in solutions.structured_conc]
specifications [section, in exercises.specifications]
specifications [section, in solutions.specifications]
specifications [library]
specifications [library]
spec1 [module, in exercises.counter]
spec1 [module, in solutions.counter]
spec1.alloc_initial_state [lemma, in exercises.counter]
spec1.alloc_initial_state [lemma, in solutions.counter]
spec1.incr_spec [lemma, in exercises.counter]
spec1.incr_spec [lemma, in solutions.counter]
spec1.is_counter_persistent [instance, in exercises.counter]
spec1.is_counter [definition, in exercises.counter]
spec1.is_counter3 [definition, in exercises.counter]
spec1.is_counter2 [definition, in exercises.counter]
spec1.is_counter1 [definition, in exercises.counter]
spec1.is_counter_persistent [instance, in solutions.counter]
spec1.is_counter [definition, in solutions.counter]
spec1.is_counter3 [definition, in solutions.counter]
spec1.is_counter2 [definition, in solutions.counter]
spec1.is_counter1 [definition, in solutions.counter]
spec1.mk_counter_spec [lemma, in exercises.counter]
spec1.mk_counter_spec [lemma, in solutions.counter]
spec1.par_incr [lemma, in exercises.counter]
spec1.par_incr [lemma, in solutions.counter]
spec1.read_spec [lemma, in exercises.counter]
spec1.read_spec [lemma, in solutions.counter]
spec1.spec1 [section, in exercises.counter]
spec1.spec1 [section, in solutions.counter]
spec1.spec1.N [variable, in exercises.counter]
spec1.spec1.N [variable, in solutions.counter]
spec1.state_valid [lemma, in exercises.counter]
spec1.state_valid [lemma, in solutions.counter]
spec1.update_state [lemma, in exercises.counter]
spec1.update_state [lemma, in solutions.counter]
spec2 [module, in exercises.counter]
spec2 [module, in solutions.counter]
spec2.alloc_initial_state [lemma, in exercises.counter]
spec2.alloc_initial_state [lemma, in solutions.counter]
spec2.incr_spec [lemma, in exercises.counter]
spec2.incr_spec [lemma, in solutions.counter]
spec2.is_counter_add [lemma, in exercises.counter]
spec2.is_counter [definition, in exercises.counter]
spec2.is_counter_add [lemma, in solutions.counter]
spec2.is_counter [definition, in solutions.counter]
spec2.mk_counter_spec [lemma, in exercises.counter]
spec2.mk_counter_spec [lemma, in solutions.counter]
spec2.read_spec_full [lemma, in exercises.counter]
spec2.read_spec [lemma, in exercises.counter]
spec2.read_spec_full [lemma, in solutions.counter]
spec2.read_spec [lemma, in solutions.counter]
spec2.spec2 [section, in exercises.counter]
spec2.spec2 [section, in solutions.counter]
spec2.spec2.N [variable, in exercises.counter]
spec2.spec2.N [variable, in solutions.counter]
spec2.state_valid_full [lemma, in exercises.counter]
spec2.state_valid [lemma, in exercises.counter]
spec2.state_valid_full [lemma, in solutions.counter]
spec2.state_valid [lemma, in solutions.counter]
spec2.update_state [lemma, in exercises.counter]
spec2.update_state [lemma, in solutions.counter]
spin_lock [library]
spin_lock [library]
Start [constructor, in exercises.custom_ra]
Start [constructor, in solutions.custom_ra]
Start_exclusive [instance, in exercises.custom_ra]
Start_exclusive [instance, in solutions.custom_ra]
state [section, in exercises.custom_ra]
state [inductive, in exercises.custom_ra]
state [section, in solutions.custom_ra]
state [inductive, in solutions.custom_ra]
stateO [definition, in exercises.custom_ra]
stateO [definition, in solutions.custom_ra]
stateR [definition, in exercises.custom_ra]
stateR [definition, in solutions.custom_ra]
state_inv [definition, in exercises.custom_ra]
state_bupd [lemma, in exercises.custom_ra]
state_valid [lemma, in exercises.custom_ra]
state_update [lemma, in exercises.custom_ra]
state_cmra_discrete [instance, in exercises.custom_ra]
state_ra_mixin [lemma, in exercises.custom_ra]
state_valid_instance [instance, in exercises.custom_ra]
state_pcore_instance [instance, in exercises.custom_ra]
state_op_instance [instance, in exercises.custom_ra]
state_leibniz_equiv [instance, in exercises.custom_ra]
state_equiv_equivalence [instance, in exercises.custom_ra]
state_equiv_instance [instance, in exercises.custom_ra]
state_sind [definition, in exercises.custom_ra]
state_rec [definition, in exercises.custom_ra]
state_ind [definition, in exercises.custom_ra]
state_rect [definition, in exercises.custom_ra]
state_inv [definition, in solutions.custom_ra]
state_bupd [lemma, in solutions.custom_ra]
state_valid [lemma, in solutions.custom_ra]
state_update [lemma, in solutions.custom_ra]
state_cmra_discrete [instance, in solutions.custom_ra]
state_ra_mixin [lemma, in solutions.custom_ra]
state_valid_instance [instance, in solutions.custom_ra]
state_pcore_instance [instance, in solutions.custom_ra]
state_op_instance [instance, in solutions.custom_ra]
state_leibniz_equiv [instance, in solutions.custom_ra]
state_equiv_equivalence [instance, in solutions.custom_ra]
state_equiv_instance [instance, in solutions.custom_ra]
state_sind [definition, in solutions.custom_ra]
state_rec [definition, in solutions.custom_ra]
state_ind [definition, in solutions.custom_ra]
state_rect [definition, in solutions.custom_ra]
step [inductive, in solutions.adequacy]
step [inductive, in exercises.adequacy]
step_sind [definition, in solutions.adequacy]
step_ind [definition, in solutions.adequacy]
step_atomic [constructor, in solutions.adequacy]
step_sind [definition, in exercises.adequacy]
step_ind [definition, in exercises.adequacy]
step_atomic [constructor, in exercises.adequacy]
store [definition, in solutions.lang]
store [definition, in exercises.lang]
stream [record, in exercises.ofe]
stream [record, in solutions.ofe]
streamO [definition, in exercises.ofe]
streamO [definition, in solutions.ofe]
stream_map_ne [instance, in exercises.ofe]
stream_map_nth [lemma, in exercises.ofe]
stream_map_alt_correct [lemma, in exercises.ofe]
stream_map_alt_unfold [lemma, in exercises.ofe]
stream_map_alt [definition, in exercises.ofe]
stream_map_pre_contractive [instance, in exercises.ofe]
stream_map_pre [definition, in exercises.ofe]
stream_map [definition, in exercises.ofe]
stream_inhabited [instance, in exercises.ofe]
stream_cofe [instance, in exercises.ofe]
stream_ofe_mixin [lemma, in exercises.ofe]
stream_dist_instance [instance, in exercises.ofe]
stream_equiv_instance [instance, in exercises.ofe]
stream_map_ne [instance, in solutions.ofe]
stream_map_nth [lemma, in solutions.ofe]
stream_map_alt_correct [lemma, in solutions.ofe]
stream_map_alt_unfold [lemma, in solutions.ofe]
stream_map_alt [definition, in solutions.ofe]
stream_map_pre_contractive [instance, in solutions.ofe]
stream_map_pre [definition, in solutions.ofe]
stream_map [definition, in solutions.ofe]
stream_inhabited [instance, in solutions.ofe]
stream_cofe [instance, in solutions.ofe]
stream_ofe_mixin [lemma, in solutions.ofe]
stream_dist_instance [instance, in solutions.ofe]
stream_equiv_instance [instance, in solutions.ofe]
structured_conc [library]
structured_conc [library]
sums [definition, in solutions.lang]
sums [definition, in exercises.lang]
sum_list_spec [lemma, in solutions.linked_lists]
sum_list [definition, in solutions.linked_lists]
sum_list_spec [lemma, in exercises.linked_lists]
sum_list [definition, in exercises.linked_lists]
swap [definition, in exercises.specifications]
swap [definition, in solutions.specifications]
swap_swap_spec [lemma, in exercises.specifications]
swap_spec [lemma, in exercises.specifications]
swap_swap_spec [lemma, in solutions.specifications]
swap_spec [lemma, in solutions.specifications]
T
tail [projection, in exercises.ofe]tail [projection, in solutions.ofe]
tail_anti_contractive [instance, in exercises.ofe]
tail_proper [instance, in exercises.ofe]
tail_anti_contractive [instance, in solutions.ofe]
tail_proper [instance, in solutions.ofe]
take_2_steps [lemma, in solutions.later]
take_2_steps [lemma, in exercises.later]
thread_spec [lemma, in exercises.custom_ra]
thread_spec [lemma, in solutions.custom_ra]
ticket_lock [library]
ticket_lock [library]
timeless [section, in solutions.timeless]
timeless [section, in exercises.timeless]
timeless [library]
timeless [library]
tok [definition, in solutions.resource_algebra]
tok [definition, in exercises.resource_algebra]
token [definition, in solutions.resource_algebra]
token [section, in solutions.resource_algebra]
token [definition, in exercises.resource_algebra]
token [section, in exercises.resource_algebra]
token_alloc [lemma, in solutions.resource_algebra]
token_exclusive [lemma, in solutions.resource_algebra]
token_token_bot [lemma, in solutions.resource_algebra]
token_valid [lemma, in solutions.resource_algebra]
token_alloc [lemma, in exercises.resource_algebra]
token_exclusive [lemma, in exercises.resource_algebra]
token_token_bot [lemma, in exercises.resource_algebra]
token_valid [lemma, in exercises.resource_algebra]
to_agree_included [lemma, in solutions.resource_algebra]
to_agree_included [lemma, in exercises.resource_algebra]
true_intro [lemma, in exercises.pure]
true_intro [lemma, in solutions.pure]
tuples [definition, in solutions.lang]
tuples [definition, in exercises.lang]
U
upd_idemp [lemma, in solutions.resource_algebra]upd_wp [lemma, in solutions.resource_algebra]
upd_assumption_fail [lemma, in solutions.resource_algebra]
upd_assumption' [lemma, in solutions.resource_algebra]
upd_assumption [lemma, in solutions.resource_algebra]
upd_intro [lemma, in solutions.resource_algebra]
upd_idemp [lemma, in exercises.resource_algebra]
upd_wp [lemma, in exercises.resource_algebra]
upd_assumption_fail [lemma, in exercises.resource_algebra]
upd_assumption' [lemma, in exercises.resource_algebra]
upd_assumption [lemma, in exercises.resource_algebra]
upd_intro [lemma, in exercises.resource_algebra]
W
wait [definition, in exercises.ticket_lock]wait [definition, in solutions.ticket_lock]
wait_spec [lemma, in exercises.ticket_lock]
wait_spec [lemma, in solutions.ticket_lock]
wand_pure [lemma, in exercises.pure]
wand_adj [lemma, in exercises.basics]
wand_adj_1 [lemma, in exercises.basics]
wand_pure [lemma, in solutions.pure]
wand_adj [lemma, in solutions.basics]
wand_adj_1 [lemma, in solutions.basics]
wp_prog [lemma, in exercises.invariants]
wp_prog [lemma, in exercises.invariants]
wp_prog [lemma, in solutions.invariants]
wp_prog [lemma, in solutions.invariants]
Z
zeros [definition, in exercises.ofe]zeros [definition, in solutions.ofe]
other
_ ||| _ (expr_scope) [notation, in exercises.structured_conc]_ ||| _ (expr_scope) [notation, in solutions.structured_conc]
_ ||| _ (val_scope) [notation, in exercises.structured_conc]
_ ||| _ (val_scope) [notation, in solutions.structured_conc]
Notation Index
P
_ ⊢ _ [in exercises.pure]_ ⊢ _ [in solutions.pure]
⊢ _ [in exercises.pure]
⊢ _ [in solutions.pure]
other
_ ||| _ (expr_scope) [in exercises.structured_conc]_ ||| _ (expr_scope) [in solutions.structured_conc]
_ ||| _ (val_scope) [in exercises.structured_conc]
_ ||| _ (val_scope) [in solutions.structured_conc]
Module Index
S
spec1 [in exercises.counter]spec1 [in solutions.counter]
spec2 [in exercises.counter]
spec2 [in solutions.counter]
Variable Index
P
parallel_add.N [in exercises.structured_conc]parallel_add.N [in solutions.structured_conc]
proofs.inv_intro.N [in exercises.invariants]
proofs.inv_intro.N [in solutions.invariants]
proofs.N [in exercises.invariants]
proofs.N [in exercises.invariants]
proofs.N [in exercises.spin_lock]
proofs.N [in solutions.spin_lock]
proofs.N [in exercises.ticket_lock]
proofs.N [in solutions.ticket_lock]
proofs.N [in exercises.custom_ra]
proofs.N [in solutions.invariants]
proofs.N [in solutions.invariants]
proofs.N [in solutions.custom_ra]
S
spawn.N [in exercises.structured_conc]spawn.N [in solutions.structured_conc]
spec1.spec1.N [in exercises.counter]
spec1.spec1.N [in solutions.counter]
spec2.spec2.N [in exercises.counter]
spec2.spec2.N [in solutions.counter]
Library Index
A
adequacyadequacy
arrays
arrays
B
basicsbasics
C
countercounter
custom_ra
custom_ra
G
gr_predicatesgr_predicates
I
invariantsinvariants
L
langlang
later
later
linked_lists
linked_lists
M
merge_sortmerge_sort
O
ofeofe
P
persistentlypersistently
pure
pure
R
resource_algebraresource_algebra
S
specificationsspecifications
spin_lock
spin_lock
structured_conc
structured_conc
T
ticket_lockticket_lock
timeless
timeless
Lemma Index
A
abstr_not_pure [in exercises.pure]abstr_not_pure [in solutions.pure]
acquire_spec [in exercises.spin_lock]
acquire_spec [in solutions.spin_lock]
acquire_spec [in exercises.ticket_lock]
acquire_spec [in solutions.ticket_lock]
agree_valid_opL [in solutions.resource_algebra]
agree_dfrac_op [in solutions.resource_algebra]
agree_dfrac [in solutions.resource_algebra]
agree_core [in solutions.resource_algebra]
agree_valid [in solutions.resource_algebra]
agree_valid_opL [in exercises.resource_algebra]
agree_dfrac_op [in exercises.resource_algebra]
agree_dfrac [in exercises.resource_algebra]
agree_core [in exercises.resource_algebra]
agree_valid [in exercises.resource_algebra]
alloc_Start [in exercises.custom_ra]
alloc_Start [in solutions.custom_ra]
and_pure [in exercises.pure]
and_pure [in solutions.pure]
append_spec [in solutions.linked_lists]
append_spec [in exercises.linked_lists]
arith_spec [in exercises.specifications]
arith_spec [in solutions.specifications]
asdfd [in exercises.basics]
asm [in exercises.basics]
asm [in solutions.basics]
asmb [in exercises.basics]
asm_pure [in exercises.pure]
asm_pure [in solutions.pure]
B
body_spec [in exercises.custom_ra]body_spec [in solutions.custom_ra]
C
cas_spec [in exercises.specifications]cas_spec [in solutions.specifications]
cmpXchg_0_to_10_spec [in exercises.specifications]
cmpXchg_0_to_10_spec [in solutions.specifications]
copy_spec [in solutions.arrays]
copy_to_spec [in solutions.arrays]
copy_spec [in exercises.arrays]
copy_to_spec [in exercises.arrays]
counter_spec [in exercises.persistently]
counter_spec [in solutions.persistently]
count_spec [in solutions.later]
count_spec [in exercises.later]
D
dfrac_alloc_one [in solutions.resource_algebra]dfrac_update_own_both [in solutions.resource_algebra]
dfrac_update_own_own [in solutions.resource_algebra]
dfrac_update_ident [in solutions.resource_algebra]
dfrac_pre_own_both [in solutions.resource_algebra]
dfrac_pre_disc_both [in solutions.resource_algebra]
dfrac_pre_own [in solutions.resource_algebra]
dfrac_core_both [in solutions.resource_algebra]
dfrac_core_discarded [in solutions.resource_algebra]
dfrac_core_own [in solutions.resource_algebra]
dfrac_invalid_own [in solutions.resource_algebra]
dfrac_valid_discarded [in solutions.resource_algebra]
dfrac_valid_own [in solutions.resource_algebra]
dfrac_op_comm [in solutions.resource_algebra]
dfrac_op_assoc [in solutions.resource_algebra]
dfrac_op_frac_both [in solutions.resource_algebra]
dfrac_op_both_disc [in solutions.resource_algebra]
dfrac_op_both [in solutions.resource_algebra]
dfrac_op_disc [in solutions.resource_algebra]
dfrac_op2 [in solutions.resource_algebra]
dfrac_op [in solutions.resource_algebra]
dfrac_frac_equiv [in solutions.resource_algebra]
dfrac_equiv_leibniz [in solutions.resource_algebra]
dfrac_alloc_one [in exercises.resource_algebra]
dfrac_update_own_both [in exercises.resource_algebra]
dfrac_update_own_own [in exercises.resource_algebra]
dfrac_update_ident [in exercises.resource_algebra]
dfrac_pre_own_both [in exercises.resource_algebra]
dfrac_pre_disc_both [in exercises.resource_algebra]
dfrac_pre_own [in exercises.resource_algebra]
dfrac_core_both [in exercises.resource_algebra]
dfrac_core_discarded [in exercises.resource_algebra]
dfrac_core_own [in exercises.resource_algebra]
dfrac_invalid_own [in exercises.resource_algebra]
dfrac_valid_discarded [in exercises.resource_algebra]
dfrac_valid_own [in exercises.resource_algebra]
dfrac_op_comm [in exercises.resource_algebra]
dfrac_op_assoc [in exercises.resource_algebra]
dfrac_op_frac_both [in exercises.resource_algebra]
dfrac_op_both_disc [in exercises.resource_algebra]
dfrac_op_both [in exercises.resource_algebra]
dfrac_op_disc [in exercises.resource_algebra]
dfrac_op2 [in exercises.resource_algebra]
dfrac_op [in exercises.resource_algebra]
dfrac_frac_equiv [in exercises.resource_algebra]
dfrac_equiv_leibniz [in exercises.resource_algebra]
disagree_dfrac [in solutions.resource_algebra]
disagree_dfrac [in exercises.resource_algebra]
E
eq_elm [in exercises.pure]eq_5_5 [in exercises.pure]
eq_elm [in solutions.pure]
eq_5_5 [in solutions.pure]
excl_op [in solutions.resource_algebra]
excl_bot_invalid [in solutions.resource_algebra]
excl_valid [in solutions.resource_algebra]
excl_core [in solutions.resource_algebra]
excl_op [in exercises.resource_algebra]
excl_bot_invalid [in exercises.resource_algebra]
excl_valid [in exercises.resource_algebra]
excl_core [in exercises.resource_algebra]
F
first_is_5 [in exercises.persistently]first_is_5 [in exercises.persistently]
first_is_5 [in solutions.persistently]
first_is_5 [in solutions.persistently]
fold_right_spec [in solutions.linked_lists]
fold_right_spec [in exercises.linked_lists]
fun2stream_nth [in exercises.ofe]
fun2stream_nth [in solutions.ofe]
H
hoare_triple_dfrac [in solutions.resource_algebra]hoare_triple_dfrac [in exercises.resource_algebra]
I
inc_spec [in solutions.arrays]inc_spec [in solutions.linked_lists]
inc_spec [in exercises.linked_lists]
inc_spec [in exercises.arrays]
inv_alloc_loc [in exercises.invariants]
inv_open_example [in exercises.invariants]
inv_open_example_attempt_2 [in exercises.invariants]
inv_open_example_attempt_1 [in exercises.invariants]
inv_open_fail [in exercises.invariants]
inv_persist [in exercises.invariants]
inv_timeless' [in solutions.timeless]
inv_timeless [in solutions.timeless]
inv_alloc_loc [in solutions.invariants]
inv_open_example [in solutions.invariants]
inv_open_example_attempt_2 [in solutions.invariants]
inv_open_example_attempt_1 [in solutions.invariants]
inv_open_fail [in solutions.invariants]
inv_persist [in solutions.invariants]
inv_timeless' [in exercises.timeless]
inv_timeless [in exercises.timeless]
is_list_rec_correct [in exercises.gr_predicates]
is_list_rec_ind [in exercises.gr_predicates]
is_list_rec_unfold [in exercises.gr_predicates]
is_list_rec_correct [in solutions.gr_predicates]
is_list_rec_ind [in solutions.gr_predicates]
is_list_rec_unfold [in solutions.gr_predicates]
J
join_spec [in exercises.structured_conc]join_spec [in exercises.structured_conc]
join_spec [in solutions.structured_conc]
join_spec [in solutions.structured_conc]
L
lambda_spec [in exercises.specifications]lambda_spec [in solutions.specifications]
later_timeless_strip [in solutions.timeless]
later_store' [in solutions.timeless]
later_store [in solutions.timeless]
later_timeless_fup' [in solutions.timeless]
later_timeless_fup [in solutions.timeless]
later_points_to [in solutions.later]
later_impl [in solutions.later]
later_sep [in solutions.later]
later_weak [in solutions.later]
later_mono' [in solutions.later]
later_mono [in solutions.later]
later_points_to [in exercises.later]
later_impl [in exercises.later]
later_sep [in exercises.later]
later_weak [in exercises.later]
later_mono' [in exercises.later]
later_mono [in exercises.later]
later_timeless_strip [in exercises.timeless]
later_store' [in exercises.timeless]
later_store [in exercises.timeless]
later_timeless_fup' [in exercises.timeless]
later_timeless_fup [in exercises.timeless]
locked_excl [in exercises.spin_lock]
locked_alloc [in exercises.spin_lock]
locked_excl [in solutions.spin_lock]
locked_alloc [in solutions.spin_lock]
locked_excl [in exercises.ticket_lock]
locked_excl [in solutions.ticket_lock]
M
merge_sort_spec [in solutions.merge_sort]merge_sort_inner_spec [in solutions.merge_sort]
merge_spec [in solutions.merge_sort]
merge_sort_spec [in exercises.merge_sort]
merge_sort_inner_spec [in exercises.merge_sort]
merge_spec [in exercises.merge_sort]
mk_lock_spec [in exercises.spin_lock]
mk_lock_spec [in solutions.spin_lock]
mk_lock_spec [in exercises.ticket_lock]
mk_lock_spec [in solutions.ticket_lock]
modus_ponens [in exercises.basics]
modus_ponens [in solutions.basics]
N
not_in_pers_context [in exercises.persistently]not_in_pers_context [in solutions.persistently]
O
only_read [in exercises.persistently]only_read [in solutions.persistently]
or_elim [in exercises.basics]
or_comm [in exercises.basics]
or_elim [in solutions.basics]
or_comm [in solutions.basics]
own_dfrac_update [in solutions.resource_algebra]
own_dfrac_both_disc [in solutions.resource_algebra]
own_dfrac_disc_persistent [in solutions.resource_algebra]
own_token_exclusive' [in solutions.resource_algebra]
own_token_exclusive [in solutions.resource_algebra]
own_op_dfrac [in solutions.resource_algebra]
own_dfrac_update [in exercises.resource_algebra]
own_dfrac_both_disc [in exercises.resource_algebra]
own_dfrac_disc_persistent [in exercises.resource_algebra]
own_token_exclusive' [in exercises.resource_algebra]
own_token_exclusive [in exercises.resource_algebra]
own_op_dfrac [in exercises.resource_algebra]
P
pair_pcore_dfrac [in solutions.resource_algebra]pair_pcore_some [in solutions.resource_algebra]
pair_pcore_dfrac [in exercises.resource_algebra]
pair_pcore_some [in exercises.resource_algebra]
parallel_add_spec [in exercises.structured_conc]
parallel_add_spec [in solutions.structured_conc]
par_read_spec [in exercises.persistently]
par_read_write_spec [in exercises.persistently]
par_client_spec [in exercises.specifications]
par_client_spec [in solutions.specifications]
par_read_spec [in solutions.persistently]
par_read_write_spec [in solutions.persistently]
par_spec [in exercises.structured_conc]
par_spec [in solutions.structured_conc]
pers_all [in exercises.persistently]
pers_sep [in exercises.persistently]
pers_idemp [in exercises.persistently]
pers_intro [in exercises.persistently]
pers_dup [in exercises.persistently]
pers_context [in exercises.persistently]
pers_all [in solutions.persistently]
pers_sep [in solutions.persistently]
pers_idemp [in solutions.persistently]
pers_intro [in solutions.persistently]
pers_dup [in solutions.persistently]
pers_context [in solutions.persistently]
power2_alt_correct [in exercises.ofe]
power2_alt_unfold [in exercises.ofe]
power2_unfold [in exercises.ofe]
power2_helper_unfold [in exercises.ofe]
power2_alt_correct [in solutions.ofe]
power2_alt_unfold [in solutions.ofe]
power2_unfold [in solutions.ofe]
power2_helper_unfold [in solutions.ofe]
prog_spec [in exercises.spin_lock]
prog_adequacy [in solutions.adequacy]
prog_add_2_spec'' [in exercises.specifications]
prog_add_2_spec' [in exercises.specifications]
prog_spec_2 [in exercises.specifications]
prog_add_2_spec [in exercises.specifications]
prog_spec [in exercises.specifications]
prog_spec [in solutions.spin_lock]
prog_add_2_spec'' [in solutions.specifications]
prog_add_2_spec' [in solutions.specifications]
prog_spec_2 [in solutions.specifications]
prog_add_2_spec [in solutions.specifications]
prog_spec [in solutions.specifications]
prog_spec [in exercises.custom_ra]
prog_adequacy [in exercises.adequacy]
prog_spec [in solutions.custom_ra]
prog2_spec [in exercises.invariants]
prog2_spec [in solutions.invariants]
pt_persist [in exercises.persistently]
pt_split [in exercises.persistently]
pt_not_dupl [in exercises.specifications]
pt_not_dupl [in solutions.specifications]
pt_persist [in solutions.persistently]
pt_split [in solutions.persistently]
pure_adj2 [in exercises.pure]
pure_adj1 [in exercises.pure]
pure_adj2 [in solutions.pure]
pure_adj1 [in solutions.pure]
R
release_spec [in exercises.spin_lock]release_spec [in solutions.spin_lock]
release_spec [in exercises.ticket_lock]
release_spec [in solutions.ticket_lock]
repeat_with_sep_alt_correct [in exercises.ofe]
repeat_with_sep_alt_unfold [in exercises.ofe]
repeat_with_sep_unfold [in exercises.ofe]
repeat_with_sep_helper_unfold [in exercises.ofe]
repeat_with_sep_alt_correct [in solutions.ofe]
repeat_with_sep_alt_unfold [in solutions.ofe]
repeat_with_sep_unfold [in solutions.ofe]
repeat_with_sep_helper_unfold [in solutions.ofe]
reverse_spec [in solutions.arrays]
reverse_spec [in solutions.linked_lists]
reverse_append_spec [in solutions.linked_lists]
reverse_spec [in exercises.linked_lists]
reverse_append_spec [in exercises.linked_lists]
reverse_spec [in exercises.arrays]
S
sep_pure [in exercises.pure]sep_all_distr [in exercises.basics]
sep_ex_distr [in exercises.basics]
sep_or_distr [in exercises.basics]
sep_comm_v2 [in exercises.basics]
sep_assoc_1 [in exercises.basics]
sep_comm [in exercises.basics]
sep_pure [in solutions.pure]
sep_all_distr [in solutions.basics]
sep_ex_distr [in solutions.basics]
sep_or_distr [in solutions.basics]
sep_comm_v2 [in solutions.basics]
sep_assoc_1 [in solutions.basics]
sep_comm [in solutions.basics]
spawn_spec [in exercises.structured_conc]
spawn_spec [in solutions.structured_conc]
spec1.alloc_initial_state [in exercises.counter]
spec1.alloc_initial_state [in solutions.counter]
spec1.incr_spec [in exercises.counter]
spec1.incr_spec [in solutions.counter]
spec1.mk_counter_spec [in exercises.counter]
spec1.mk_counter_spec [in solutions.counter]
spec1.par_incr [in exercises.counter]
spec1.par_incr [in solutions.counter]
spec1.read_spec [in exercises.counter]
spec1.read_spec [in solutions.counter]
spec1.state_valid [in exercises.counter]
spec1.state_valid [in solutions.counter]
spec1.update_state [in exercises.counter]
spec1.update_state [in solutions.counter]
spec2.alloc_initial_state [in exercises.counter]
spec2.alloc_initial_state [in solutions.counter]
spec2.incr_spec [in exercises.counter]
spec2.incr_spec [in solutions.counter]
spec2.is_counter_add [in exercises.counter]
spec2.is_counter_add [in solutions.counter]
spec2.mk_counter_spec [in exercises.counter]
spec2.mk_counter_spec [in solutions.counter]
spec2.read_spec_full [in exercises.counter]
spec2.read_spec [in exercises.counter]
spec2.read_spec_full [in solutions.counter]
spec2.read_spec [in solutions.counter]
spec2.state_valid_full [in exercises.counter]
spec2.state_valid [in exercises.counter]
spec2.state_valid_full [in solutions.counter]
spec2.state_valid [in solutions.counter]
spec2.update_state [in exercises.counter]
spec2.update_state [in solutions.counter]
state_bupd [in exercises.custom_ra]
state_valid [in exercises.custom_ra]
state_update [in exercises.custom_ra]
state_ra_mixin [in exercises.custom_ra]
state_bupd [in solutions.custom_ra]
state_valid [in solutions.custom_ra]
state_update [in solutions.custom_ra]
state_ra_mixin [in solutions.custom_ra]
stream_map_nth [in exercises.ofe]
stream_map_alt_correct [in exercises.ofe]
stream_map_alt_unfold [in exercises.ofe]
stream_ofe_mixin [in exercises.ofe]
stream_map_nth [in solutions.ofe]
stream_map_alt_correct [in solutions.ofe]
stream_map_alt_unfold [in solutions.ofe]
stream_ofe_mixin [in solutions.ofe]
sum_list_spec [in solutions.linked_lists]
sum_list_spec [in exercises.linked_lists]
swap_swap_spec [in exercises.specifications]
swap_spec [in exercises.specifications]
swap_swap_spec [in solutions.specifications]
swap_spec [in solutions.specifications]
T
take_2_steps [in solutions.later]take_2_steps [in exercises.later]
thread_spec [in exercises.custom_ra]
thread_spec [in solutions.custom_ra]
token_alloc [in solutions.resource_algebra]
token_exclusive [in solutions.resource_algebra]
token_token_bot [in solutions.resource_algebra]
token_valid [in solutions.resource_algebra]
token_alloc [in exercises.resource_algebra]
token_exclusive [in exercises.resource_algebra]
token_token_bot [in exercises.resource_algebra]
token_valid [in exercises.resource_algebra]
to_agree_included [in solutions.resource_algebra]
to_agree_included [in exercises.resource_algebra]
true_intro [in exercises.pure]
true_intro [in solutions.pure]
U
upd_idemp [in solutions.resource_algebra]upd_wp [in solutions.resource_algebra]
upd_assumption_fail [in solutions.resource_algebra]
upd_assumption' [in solutions.resource_algebra]
upd_assumption [in solutions.resource_algebra]
upd_intro [in solutions.resource_algebra]
upd_idemp [in exercises.resource_algebra]
upd_wp [in exercises.resource_algebra]
upd_assumption_fail [in exercises.resource_algebra]
upd_assumption' [in exercises.resource_algebra]
upd_assumption [in exercises.resource_algebra]
upd_intro [in exercises.resource_algebra]
W
wait_spec [in exercises.ticket_lock]wait_spec [in solutions.ticket_lock]
wand_pure [in exercises.pure]
wand_adj [in exercises.basics]
wand_adj_1 [in exercises.basics]
wand_pure [in solutions.pure]
wand_adj [in solutions.basics]
wand_adj_1 [in solutions.basics]
wp_prog [in exercises.invariants]
wp_prog [in exercises.invariants]
wp_prog [in solutions.invariants]
wp_prog [in solutions.invariants]
Constructor Index
F
Final [in exercises.custom_ra]Final [in solutions.custom_ra]
I
Invalid [in exercises.custom_ra]Invalid [in solutions.custom_ra]
S
Start [in exercises.custom_ra]Start [in solutions.custom_ra]
step_atomic [in solutions.adequacy]
step_atomic [in exercises.adequacy]
Inductive Index
S
state [in exercises.custom_ra]state [in solutions.custom_ra]
step [in solutions.adequacy]
step [in exercises.adequacy]
Projection Index
H
head [in exercises.ofe]head [in solutions.ofe]
T
tail [in exercises.ofe]tail [in solutions.ofe]
Section Index
A
agree [in solutions.resource_algebra]agree [in exercises.resource_algebra]
E
exclusive [in solutions.resource_algebra]exclusive [in exercises.resource_algebra]
G
ghost [in solutions.resource_algebra]ghost [in exercises.resource_algebra]
H
heaplang [in solutions.lang]heaplang [in exercises.lang]
L
later [in solutions.later]later [in exercises.later]
linked_lists [in solutions.linked_lists]
linked_lists [in exercises.linked_lists]
O
ofe [in exercises.ofe]ofe [in solutions.ofe]
P
par [in exercises.structured_conc]par [in solutions.structured_conc]
parallel_add [in exercises.structured_conc]
parallel_add [in solutions.structured_conc]
persistently [in exercises.persistently]
persistently [in solutions.persistently]
product [in solutions.resource_algebra]
product [in exercises.resource_algebra]
proofs [in exercises.invariants]
proofs [in exercises.invariants]
proofs [in exercises.spin_lock]
proofs [in exercises.pure]
proofs [in solutions.spin_lock]
proofs [in exercises.ticket_lock]
proofs [in solutions.arrays]
proofs [in solutions.ticket_lock]
proofs [in exercises.gr_predicates]
proofs [in solutions.merge_sort]
proofs [in exercises.custom_ra]
proofs [in solutions.invariants]
proofs [in solutions.invariants]
proofs [in solutions.gr_predicates]
proofs [in exercises.merge_sort]
proofs [in exercises.basics]
proofs [in solutions.custom_ra]
proofs [in solutions.pure]
proofs [in solutions.basics]
proofs [in exercises.arrays]
proofs.inv_intro [in exercises.invariants]
proofs.inv_intro [in solutions.invariants]
properties [in exercises.custom_ra]
properties [in solutions.custom_ra]
S
spawn [in exercises.structured_conc]spawn [in solutions.structured_conc]
specifications [in exercises.specifications]
specifications [in solutions.specifications]
spec1.spec1 [in exercises.counter]
spec1.spec1 [in solutions.counter]
spec2.spec2 [in exercises.counter]
spec2.spec2 [in solutions.counter]
state [in exercises.custom_ra]
state [in solutions.custom_ra]
T
timeless [in solutions.timeless]timeless [in exercises.timeless]
token [in solutions.resource_algebra]
token [in exercises.resource_algebra]
Instance Index
F
Final_core_id [in exercises.custom_ra]Final_core_id [in solutions.custom_ra]
I
is_list_pre_mono [in exercises.gr_predicates]is_list_pre_mono [in solutions.gr_predicates]
M
myPredFix_persistent [in exercises.persistently]myPredFix_persistent [in solutions.persistently]
myPredicate_persistent' [in exercises.persistently]
myPredicate_persistent [in exercises.persistently]
myPredicate_persistent' [in solutions.persistently]
myPredicate_persistent [in solutions.persistently]
N
nth_proper [in exercises.ofe]nth_proper [in solutions.ofe]
P
power2_pre_contractive [in exercises.ofe]power2_pre_contractive [in solutions.ofe]
R
repeat_with_sep_contractive [in exercises.ofe]repeat_with_sep_contractive [in solutions.ofe]
S
sapp_proper [in exercises.ofe]sapp_ne [in exercises.ofe]
sapp_proper [in solutions.ofe]
sapp_ne [in solutions.ofe]
SCons_proper [in exercises.ofe]
SCons_ne [in exercises.ofe]
SCons_contractive [in exercises.ofe]
SCons_proper [in solutions.ofe]
SCons_ne [in solutions.ofe]
SCons_contractive [in solutions.ofe]
spec1.is_counter_persistent [in exercises.counter]
spec1.is_counter_persistent [in solutions.counter]
Start_exclusive [in exercises.custom_ra]
Start_exclusive [in solutions.custom_ra]
state_cmra_discrete [in exercises.custom_ra]
state_valid_instance [in exercises.custom_ra]
state_pcore_instance [in exercises.custom_ra]
state_op_instance [in exercises.custom_ra]
state_leibniz_equiv [in exercises.custom_ra]
state_equiv_equivalence [in exercises.custom_ra]
state_equiv_instance [in exercises.custom_ra]
state_cmra_discrete [in solutions.custom_ra]
state_valid_instance [in solutions.custom_ra]
state_pcore_instance [in solutions.custom_ra]
state_op_instance [in solutions.custom_ra]
state_leibniz_equiv [in solutions.custom_ra]
state_equiv_equivalence [in solutions.custom_ra]
state_equiv_instance [in solutions.custom_ra]
stream_map_ne [in exercises.ofe]
stream_map_pre_contractive [in exercises.ofe]
stream_inhabited [in exercises.ofe]
stream_cofe [in exercises.ofe]
stream_dist_instance [in exercises.ofe]
stream_equiv_instance [in exercises.ofe]
stream_map_ne [in solutions.ofe]
stream_map_pre_contractive [in solutions.ofe]
stream_inhabited [in solutions.ofe]
stream_cofe [in solutions.ofe]
stream_dist_instance [in solutions.ofe]
stream_equiv_instance [in solutions.ofe]
T
tail_anti_contractive [in exercises.ofe]tail_proper [in exercises.ofe]
tail_anti_contractive [in solutions.ofe]
tail_proper [in solutions.ofe]
Definition Index
A
acquire [in exercises.spin_lock]acquire [in solutions.spin_lock]
acquire [in exercises.ticket_lock]
acquire [in solutions.ticket_lock]
all [in exercises.gr_predicates]
all [in solutions.gr_predicates]
alloc [in solutions.lang]
alloc [in exercises.lang]
and_success [in exercises.basics]
and_fail [in exercises.basics]
and_success [in solutions.basics]
and_fail [in solutions.basics]
append [in solutions.linked_lists]
append [in exercises.linked_lists]
arith [in solutions.lang]
arith [in exercises.specifications]
arith [in exercises.lang]
arith [in solutions.specifications]
B
booleans [in solutions.lang]booleans [in exercises.lang]
C
cas [in solutions.lang]cas [in exercises.specifications]
cas [in exercises.lang]
cas [in solutions.specifications]
cfg [in solutions.adequacy]
cfg [in exercises.adequacy]
cmpxchg_suc [in solutions.lang]
cmpxchg_fail [in solutions.lang]
cmpXchg_0_to_10 [in exercises.specifications]
cmpxchg_suc [in exercises.lang]
cmpxchg_fail [in exercises.lang]
cmpXchg_0_to_10 [in solutions.specifications]
copy [in solutions.arrays]
copy [in exercises.arrays]
copy_to [in solutions.arrays]
copy_to [in exercises.arrays]
count [in solutions.later]
count [in exercises.later]
counter [in exercises.persistently]
counter [in solutions.persistently]
D
dfrac_update_disc [in solutions.resource_algebra]dfrac_update [in solutions.resource_algebra]
dfrac_update_disc [in exercises.resource_algebra]
dfrac_update [in exercises.resource_algebra]
E
excl_op_dfrac [in solutions.resource_algebra]excl_op_dfrac [in exercises.resource_algebra]
F
fold_right [in solutions.linked_lists]fold_right [in exercises.linked_lists]
fork [in solutions.lang]
fork [in exercises.lang]
fun2stream [in exercises.ofe]
fun2stream [in solutions.ofe]
H
handle_inv [in exercises.structured_conc]handle_inv1 [in exercises.structured_conc]
handle_inv [in solutions.structured_conc]
handle_inv1 [in solutions.structured_conc]
I
if_then_else [in solutions.lang]if_then_else [in exercises.lang]
inc [in solutions.arrays]
inc [in solutions.linked_lists]
inc [in exercises.linked_lists]
inc [in exercises.arrays]
incr [in exercises.counter]
incr [in solutions.counter]
isList [in solutions.linked_lists]
isList [in exercises.linked_lists]
issued [in exercises.ticket_lock]
issued [in solutions.ticket_lock]
is_lock [in exercises.spin_lock]
is_lock [in solutions.spin_lock]
is_lock [in exercises.ticket_lock]
is_lock [in solutions.ticket_lock]
is_list_rec [in exercises.gr_predicates]
is_list_pre [in exercises.gr_predicates]
is_list [in exercises.gr_predicates]
is_list_of [in exercises.gr_predicates]
is_list_rec [in solutions.gr_predicates]
is_list_pre [in solutions.gr_predicates]
is_list [in solutions.gr_predicates]
is_list_of [in solutions.gr_predicates]
J
join [in exercises.structured_conc]join [in solutions.structured_conc]
join_handle [in exercises.structured_conc]
join_handle1 [in exercises.structured_conc]
join_handle [in solutions.structured_conc]
join_handle1 [in solutions.structured_conc]
L
lambda [in solutions.lang]lambda [in exercises.specifications]
lambda [in exercises.lang]
lambda [in solutions.specifications]
lets [in solutions.lang]
lets [in exercises.lang]
load [in solutions.lang]
load [in exercises.lang]
locked [in exercises.spin_lock]
locked [in solutions.spin_lock]
locked [in exercises.ticket_lock]
locked [in solutions.ticket_lock]
locked_by [in exercises.ticket_lock]
locked_by [in solutions.ticket_lock]
lock_inv [in exercises.spin_lock]
lock_inv [in solutions.spin_lock]
lock_inv [in exercises.ticket_lock]
lock_inv [in solutions.ticket_lock]
M
merge [in solutions.merge_sort]merge [in exercises.merge_sort]
merge_sort [in solutions.merge_sort]
merge_sort_inner [in solutions.merge_sort]
merge_sort [in exercises.merge_sort]
merge_sort_inner [in exercises.merge_sort]
mk_counter [in exercises.counter]
mk_lock [in exercises.spin_lock]
mk_lock [in solutions.spin_lock]
mk_lock [in exercises.ticket_lock]
mk_lock [in solutions.ticket_lock]
mk_counter [in solutions.counter]
myPredFix [in exercises.persistently]
myPredFix [in solutions.persistently]
myPredicate [in exercises.persistently]
myPredicate [in solutions.persistently]
N
not_stuck [in solutions.adequacy]not_stuck [in exercises.adequacy]
nth [in exercises.ofe]
nth [in solutions.ofe]
O
option [in solutions.lang]option [in exercises.lang]
P
pairs [in solutions.lang]pairs [in exercises.lang]
par [in solutions.lang]
par [in exercises.lang]
par [in exercises.structured_conc]
par [in solutions.structured_conc]
parallel_add_inv [in exercises.structured_conc]
parallel_add [in exercises.structured_conc]
parallel_add_inv [in solutions.structured_conc]
parallel_add [in solutions.structured_conc]
par_read [in exercises.persistently]
par_read_write [in exercises.persistently]
par_client [in exercises.specifications]
par_client [in solutions.specifications]
par_read [in solutions.persistently]
par_read_write [in solutions.persistently]
power2 [in exercises.ofe]
power2 [in exercises.ofe]
power2 [in solutions.ofe]
power2 [in solutions.ofe]
power2_alt [in exercises.ofe]
power2_pre [in exercises.ofe]
power2_helper [in exercises.ofe]
power2_alt [in solutions.ofe]
power2_pre [in solutions.ofe]
power2_helper [in solutions.ofe]
prog [in exercises.invariants]
prog [in exercises.spin_lock]
prog [in exercises.specifications]
prog [in solutions.spin_lock]
prog [in solutions.specifications]
prog [in exercises.custom_ra]
prog [in solutions.invariants]
prog [in solutions.custom_ra]
prog_inv [in exercises.invariants]
prog_inv [in solutions.invariants]
prog2 [in exercises.invariants]
prog2 [in solutions.invariants]
prog2_inv [in exercises.invariants]
prog2_inv [in solutions.invariants]
progΣ [in solutions.adequacy]
progΣ [in exercises.adequacy]
R
RA [in exercises.ticket_lock]RA [in solutions.ticket_lock]
race [in exercises.specifications]
race [in solutions.specifications]
race_spec [in solutions.specifications]
read [in exercises.counter]
read [in solutions.counter]
recursion [in solutions.lang]
recursion [in exercises.lang]
release [in exercises.spin_lock]
release [in solutions.spin_lock]
release [in exercises.ticket_lock]
release [in solutions.ticket_lock]
repeat [in exercises.ofe]
repeat [in solutions.ofe]
repeat_with_sep_alt [in exercises.ofe]
repeat_with_sep_pre [in exercises.ofe]
repeat_with_sep [in exercises.ofe]
repeat_with_sep_helper [in exercises.ofe]
repeat_with_sep [in exercises.ofe]
repeat_with_sep_alt [in solutions.ofe]
repeat_with_sep_pre [in solutions.ofe]
repeat_with_sep [in solutions.ofe]
repeat_with_sep_helper [in solutions.ofe]
repeat_with_sep [in solutions.ofe]
reverse [in solutions.arrays]
reverse [in solutions.linked_lists]
reverse [in exercises.linked_lists]
reverse [in exercises.arrays]
reverse_append [in solutions.linked_lists]
reverse_append [in exercises.linked_lists]
S
sapp [in exercises.ofe]sapp [in solutions.ofe]
spawn [in solutions.lang]
spawn [in exercises.lang]
spawn [in exercises.structured_conc]
spawn [in solutions.structured_conc]
spec1.is_counter [in exercises.counter]
spec1.is_counter3 [in exercises.counter]
spec1.is_counter2 [in exercises.counter]
spec1.is_counter1 [in exercises.counter]
spec1.is_counter [in solutions.counter]
spec1.is_counter3 [in solutions.counter]
spec1.is_counter2 [in solutions.counter]
spec1.is_counter1 [in solutions.counter]
spec2.is_counter [in exercises.counter]
spec2.is_counter [in solutions.counter]
stateO [in exercises.custom_ra]
stateO [in solutions.custom_ra]
stateR [in exercises.custom_ra]
stateR [in solutions.custom_ra]
state_inv [in exercises.custom_ra]
state_sind [in exercises.custom_ra]
state_rec [in exercises.custom_ra]
state_ind [in exercises.custom_ra]
state_rect [in exercises.custom_ra]
state_inv [in solutions.custom_ra]
state_sind [in solutions.custom_ra]
state_rec [in solutions.custom_ra]
state_ind [in solutions.custom_ra]
state_rect [in solutions.custom_ra]
step_sind [in solutions.adequacy]
step_ind [in solutions.adequacy]
step_sind [in exercises.adequacy]
step_ind [in exercises.adequacy]
store [in solutions.lang]
store [in exercises.lang]
streamO [in exercises.ofe]
streamO [in solutions.ofe]
stream_map_alt [in exercises.ofe]
stream_map_pre [in exercises.ofe]
stream_map [in exercises.ofe]
stream_map_alt [in solutions.ofe]
stream_map_pre [in solutions.ofe]
stream_map [in solutions.ofe]
sums [in solutions.lang]
sums [in exercises.lang]
sum_list [in solutions.linked_lists]
sum_list [in exercises.linked_lists]
swap [in exercises.specifications]
swap [in solutions.specifications]
T
tok [in solutions.resource_algebra]tok [in exercises.resource_algebra]
token [in solutions.resource_algebra]
token [in exercises.resource_algebra]
tuples [in solutions.lang]
tuples [in exercises.lang]
W
wait [in exercises.ticket_lock]wait [in solutions.ticket_lock]
Z
zeros [in exercises.ofe]zeros [in solutions.ofe]
Record Index
S
stream [in exercises.ofe]stream [in solutions.ofe]
| 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 | (865 entries) |
| Notation 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 | (8 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 | _ | other | (4 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 | (20 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 | (40 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 | (396 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 | (8 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 | (4 entries) |
| Projection 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) |
| 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 | (60 entries) |
| Instance 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 | (60 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 | (259 entries) |
| Record 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) |