| 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 | (2322 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 | (89 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 | (102 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 | (116 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 | (59 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 | (765 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 | (97 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 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 | (50 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 | (43 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 | (91 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 | (342 entries) |
| Abbreviation 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 | (107 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 | (425 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 | (24 entries) |
Global Index
A
addr [library]add_opt_inj [instance, in bedrock.prelude.option]
add_opt [definition, in bedrock.prelude.option]
add_opt [section, in bedrock.prelude.option]
Alias [module, in bedrock.prelude.elpi.derive_test]
Alias.A [constructor, in bedrock.prelude.elpi.derive_test]
Alias.B [constructor, in bedrock.prelude.elpi.derive_test]
Alias.Cmd [module, in bedrock.prelude.elpi.derive_test]
Alias.Countable [module, in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasDirect [module, in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasDirect.t1_countable [definition, in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasDirect.t1_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasIndirect [module, in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasIndirect.t2_countable [definition, in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasIndirect.t2_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnVariant [module, in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnVariant.T_countable [definition, in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnVariant.T_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnAliasIndirect.t2_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnAliasIndirect [module, in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnAliasDirect.t1_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnAliasDirect [module, in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnVariant.T_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnVariant [module, in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec [module, in bedrock.prelude.elpi.derive_test]
Alias.Finite [module, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect [module, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect.t1_finite [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect.t1_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect.t1_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect.t1_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect [module, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect.t2_finite [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect.t2_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect.t2_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect.t2_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant [module, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant.T_finite [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant.T_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant.T_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant.T_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Alias.Inhabited [module, in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnAliasDirect [module, in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnAliasDirect.t1_inhabited [definition, in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnAliasIndirect [module, in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnAliasIndirect.t2_inhabited [definition, in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnVariant [module, in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnVariant.T_inhabited [definition, in bedrock.prelude.elpi.derive_test]
Alias.T [inductive, in bedrock.prelude.elpi.derive_test]
Alias.t1 [definition, in bedrock.prelude.elpi.derive_test]
Alias.t2 [definition, in bedrock.prelude.elpi.derive_test]
align_up_nonneg [lemma, in bedrock.prelude.numbers]
align_dn_nonneg [lemma, in bedrock.prelude.numbers]
align_dn_le_up [lemma, in bedrock.prelude.numbers]
align_up_mono [lemma, in bedrock.prelude.numbers]
align_up_above [lemma, in bedrock.prelude.numbers]
align_up_below [lemma, in bedrock.prelude.numbers]
align_up_divide [lemma, in bedrock.prelude.numbers]
align_dn_mono [lemma, in bedrock.prelude.numbers]
align_dn_above [lemma, in bedrock.prelude.numbers]
align_dn_below [lemma, in bedrock.prelude.numbers]
align_dn_divide [lemma, in bedrock.prelude.numbers]
align_dn_pow2 [lemma, in bedrock.prelude.numbers]
align_up [definition, in bedrock.prelude.numbers]
align_dn [definition, in bedrock.prelude.numbers]
alterN [abbreviation, in bedrock.prelude.list_numbers]
alterN_explode [lemma, in bedrock.prelude.list_numbers]
andb_right_absorb [instance, in bedrock.prelude.bool]
andb_left_absorb [instance, in bedrock.prelude.bool]
andb_right_id [instance, in bedrock.prelude.bool]
andb_left_id [instance, in bedrock.prelude.bool]
andb_assoc' [instance, in bedrock.prelude.bool]
andb_comm' [instance, in bedrock.prelude.bool]
andP [lemma, in bedrock.prelude.bool]
and_proper_r [lemma, in bedrock.prelude.base]
and_proper_l [lemma, in bedrock.prelude.base]
ap [abbreviation, in bedrock.prelude.list]
ap [section, in bedrock.prelude.list]
applicative_fmap [instance, in bedrock.prelude.base]
ap_app_r [lemma, in bedrock.prelude.list]
ap_app_l [lemma, in bedrock.prelude.list]
ap_cons_r_p [lemma, in bedrock.prelude.list]
ap_cons_l [lemma, in bedrock.prelude.list]
ap_nil_r [lemma, in bedrock.prelude.list]
ap_nil_l [lemma, in bedrock.prelude.list]
ap_Permutation [instance, in bedrock.prelude.list]
ap.A [variable, in bedrock.prelude.list]
ap.B [variable, in bedrock.prelude.list]
ap.C [variable, in bedrock.prelude.list]
attrs [module, in bedrock.prelude.page]
attrs.is_rwsx [definition, in bedrock.prelude.page]
attrs.is_rwux [definition, in bedrock.prelude.page]
attrs.is_rw [definition, in bedrock.prelude.page]
attrs.is_r [definition, in bedrock.prelude.page]
attrs.masked [definition, in bedrock.prelude.page]
attrs.masked_opt [definition, in bedrock.prelude.page]
attrs.none [definition, in bedrock.prelude.page]
attrs.nonnull [definition, in bedrock.prelude.page]
attrs.opteT [definition, in bedrock.prelude.page]
attrs.opte_mask [definition, in bedrock.prelude.page]
attrs.pteT [definition, in bedrock.prelude.page]
attrs.R [definition, in bedrock.prelude.page]
attrs.read [projection, in bedrock.prelude.page]
attrs.RW [definition, in bedrock.prelude.page]
attrs.RWX [definition, in bedrock.prelude.page]
attrs.sexec [projection, in bedrock.prelude.page]
attrs.t [record, in bedrock.prelude.page]
attrs.t_countable [instance, in bedrock.prelude.page]
attrs.t_inhabited [instance, in bedrock.prelude.page]
attrs.t_eq_dec [instance, in bedrock.prelude.page]
attrs.uexec [projection, in bedrock.prelude.page]
attrs.user [abbreviation, in bedrock.prelude.page]
attrs.W [definition, in bedrock.prelude.page]
attrs.write [projection, in bedrock.prelude.page]
avl [library]
B
base [library]base_dbs [library]
BasicTests [module, in bedrock.prelude.elpi.derive_test]
BasicTests.A1 [constructor, in bedrock.prelude.elpi.derive_test]
BasicTests.A2 [constructor, in bedrock.prelude.elpi.derive_test]
BasicTests.A2 [constructor, in bedrock.prelude.elpi.derive_test]
BasicTests.B1 [constructor, in bedrock.prelude.elpi.derive_test]
BasicTests.B2 [constructor, in bedrock.prelude.elpi.derive_test]
BasicTests.B2 [constructor, in bedrock.prelude.elpi.derive_test]
BasicTests.C1 [constructor, in bedrock.prelude.elpi.derive_test]
BasicTests.C2 [constructor, in bedrock.prelude.elpi.derive_test]
BasicTests.C2 [constructor, in bedrock.prelude.elpi.derive_test]
BasicTests.T1 [inductive, in bedrock.prelude.elpi.derive_test]
BasicTests.T1_finite [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T1_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T1_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T1_countable [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T1_inhabited [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T1_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2 [inductive, in bedrock.prelude.elpi.derive_test]
BasicTests.T2 [inductive, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_countable [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_inhabited [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
BasicTests.T2_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
basis [library]
Beta [abbreviation, in bedrock.prelude.base]
binder [projection, in bedrock.prelude.named_binder]
Binder [record, in bedrock.prelude.named_binder]
binder [constructor, in bedrock.prelude.named_binder]
Binder [inductive, in bedrock.prelude.named_binder]
Binder [section, in bedrock.prelude.named_binder]
Binder [module, in bedrock.prelude.named_binder]
bindM2 [definition, in bedrock.prelude.base]
bitmask_type_simple_mixin.to_bit_lt_card_N [lemma, in bedrock.prelude.finite]
bitmask_type_simple_mixin.to_of_bit [lemma, in bedrock.prelude.finite]
bitmask_type_simple_mixin.of_to_bit [lemma, in bedrock.prelude.finite]
bitmask_type_simple_mixin.of_bit [definition, in bedrock.prelude.finite]
bitmask_type_simple_mixin.to_bit [definition, in bedrock.prelude.finite]
bitmask_type_simple_mixin [module, in bedrock.prelude.finite]
bitmask_type.to_bit [axiom, in bedrock.prelude.finite]
bitmask_type [module, in bedrock.prelude.finite]
bitset [library]
BitsetTest [module, in bedrock.prelude.elpi.derive_test]
BitsetTest.A [constructor, in bedrock.prelude.elpi.derive_test]
BitsetTest.B [constructor, in bedrock.prelude.elpi.derive_test]
BitsetTest.C [constructor, in bedrock.prelude.elpi.derive_test]
BitsetTest.D [constructor, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature [module, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature [inductive, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature_set [module, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature_finite [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature.t [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature.to_bit [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature.t_finite [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.feature.t_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.Unnamed_thm1 [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.Unnamed_thm0 [definition, in bedrock.prelude.elpi.derive_test]
BitsetTest.Unnamed_thm [definition, in bedrock.prelude.elpi.derive_test]
bitsN [library]
Bool [module, in bedrock.prelude.bool]
bool [library]
boolP [lemma, in bedrock.prelude.bool]
bool_decide_lt_irrefl [lemma, in bedrock.prelude.list_numbers]
bool_decide_sub_move_0_r [lemma, in bedrock.prelude.list_numbers]
bool_decide_refl [lemma, in bedrock.prelude.list_numbers]
bool_decide_is_true [lemma, in bedrock.prelude.bool]
bool_decide_bool_eq [lemma, in bedrock.prelude.bool]
bool_decide_Is_true [lemma, in bedrock.prelude.bool]
bool_compare [instance, in bedrock.prelude.bool]
Bool.andb_min_r [lemma, in bedrock.prelude.bool]
Bool.andb_min_l [lemma, in bedrock.prelude.bool]
Bool.leb [definition, in bedrock.prelude.bool]
Bool.le_andb_r [lemma, in bedrock.prelude.bool]
Bool.le_andb_l [lemma, in bedrock.prelude.bool]
Bool.le_preorder [instance, in bedrock.prelude.bool]
Bool.le_pi [instance, in bedrock.prelude.bool]
Bool.le_dec [instance, in bedrock.prelude.bool]
Bool.le_leb [lemma, in bedrock.prelude.bool]
BS [module, in bedrock.prelude.bytestring]
BS [module, in bedrock.prelude.bytestring_core]
bs_compare [instance, in bedrock.prelude.bytestring_core]
bs_cmp [definition, in bedrock.prelude.bytestring_core]
bs_parse_string [instance, in bedrock.prelude.parsec]
bs_next [instance, in bedrock.prelude.parsec]
BS.append [definition, in bedrock.prelude.bytestring_core]
BS.append_right_id [instance, in bedrock.prelude.bytestring_core]
BS.append_left_id [instance, in bedrock.prelude.bytestring_core]
BS.append_alt [lemma, in bedrock.prelude.bytestring_core]
BS.append_tailrec [definition, in bedrock.prelude.bytestring_core]
BS.Buf [module, in bedrock.prelude.bytestring_core]
BS.Buf.Append [constructor, in bedrock.prelude.bytestring_core]
BS.Buf.Byte [constructor, in bedrock.prelude.bytestring_core]
BS.Buf.Concat [constructor, in bedrock.prelude.bytestring_core]
BS.Buf.concat_aux [definition, in bedrock.prelude.bytestring_core]
BS.Buf.contents [definition, in bedrock.prelude.bytestring_core]
BS.Buf.contents_aux [definition, in bedrock.prelude.bytestring_core]
BS.Buf.empty [instance, in bedrock.prelude.bytestring_core]
BS.Buf.Empty [constructor, in bedrock.prelude.bytestring_core]
BS.Buf.monoid [instance, in bedrock.prelude.bytestring_core]
BS.Buf.String [constructor, in bedrock.prelude.bytestring_core]
BS.Buf.t [inductive, in bedrock.prelude.bytestring_core]
BS.Buf.t_sind [definition, in bedrock.prelude.bytestring_core]
BS.Buf.t_rec [definition, in bedrock.prelude.bytestring_core]
BS.Buf.t_ind [definition, in bedrock.prelude.bytestring_core]
BS.Buf.t_rect [definition, in bedrock.prelude.bytestring_core]
BS.Byte [abbreviation, in bedrock.prelude.bytestring_core]
_ ++ _ (bs_scope) [notation, in bedrock.prelude.bytestring_core]
BS.Bytestring_notations.bs [abbreviation, in bedrock.prelude.bytestring_core]
BS.Bytestring_notations [module, in bedrock.prelude.bytestring_core]
BS.bytes_to_string_to_bytes [instance, in bedrock.prelude.bytestring]
BS.bytes_to_string [definition, in bedrock.prelude.bytestring]
BS.concat [definition, in bedrock.prelude.bytestring_core]
BS.concat_aux [definition, in bedrock.prelude.bytestring_core]
BS.contains [definition, in bedrock.prelude.bytestring_core]
BS.decimal_digit [definition, in bedrock.prelude.bytestring]
BS.drop [definition, in bedrock.prelude.bytestring]
BS.EmptyString [constructor, in bedrock.prelude.bytestring_core]
BS.eqb [definition, in bedrock.prelude.bytestring_core]
BS.eq_dec [definition, in bedrock.prelude.bytestring_core]
BS.index [definition, in bedrock.prelude.bytestring_core]
BS.last [definition, in bedrock.prelude.bytestring]
BS.length [definition, in bedrock.prelude.bytestring_core]
BS.of_N_decimal [definition, in bedrock.prelude.bytestring]
BS.of_string_to_string_inv [lemma, in bedrock.prelude.bytestring]
BS.of_string [definition, in bedrock.prelude.bytestring]
BS.parse [definition, in bedrock.prelude.bytestring_core]
BS.parse_inj [instance, in bedrock.prelude.bytestring_core]
BS.parse_string_inv [lemma, in bedrock.prelude.bytestring_core]
BS.parse_nil_inv [lemma, in bedrock.prelude.bytestring_core]
BS.parse_cons [lemma, in bedrock.prelude.bytestring_core]
BS.parse_nil [lemma, in bedrock.prelude.bytestring_core]
BS.parse_print_inv [lemma, in bedrock.prelude.bytestring_core]
BS.pp_N_aux [definition, in bedrock.prelude.bytestring]
BS.prefix [definition, in bedrock.prelude.bytestring_core]
BS.print [definition, in bedrock.prelude.bytestring_core]
BS.print_length [lemma, in bedrock.prelude.bytestring_core]
BS.print_append [lemma, in bedrock.prelude.bytestring_core]
BS.print_append_tailrec [lemma, in bedrock.prelude.bytestring_core]
BS.print_rev [lemma, in bedrock.prelude.bytestring_core]
BS.print_rev_append [lemma, in bedrock.prelude.bytestring_core]
BS.print_inj [instance, in bedrock.prelude.bytestring_core]
BS.print_cons_inv [lemma, in bedrock.prelude.bytestring_core]
BS.print_nil_inv [lemma, in bedrock.prelude.bytestring_core]
BS.print_string [lemma, in bedrock.prelude.bytestring_core]
BS.print_empty [lemma, in bedrock.prelude.bytestring_core]
BS.print_parse_inv [lemma, in bedrock.prelude.bytestring_core]
BS.rev [definition, in bedrock.prelude.bytestring_core]
BS.rev_app [lemma, in bedrock.prelude.bytestring_core]
BS.rev_involutive [lemma, in bedrock.prelude.bytestring_core]
BS.rev_string [lemma, in bedrock.prelude.bytestring_core]
BS.rev_empty [lemma, in bedrock.prelude.bytestring_core]
BS.rev_append [definition, in bedrock.prelude.bytestring_core]
BS.sepBy [abbreviation, in bedrock.prelude.bytestring]
BS.split_at [definition, in bedrock.prelude.bytestring]
BS.split_at_loop [definition, in bedrock.prelude.bytestring]
BS.String [constructor, in bedrock.prelude.bytestring_core]
BS.string_to_bytes [definition, in bedrock.prelude.bytestring]
BS.substring [definition, in bedrock.prelude.bytestring_core]
BS.t [inductive, in bedrock.prelude.bytestring_core]
BS.take [definition, in bedrock.prelude.bytestring]
BS.to_string_of_string_inv [lemma, in bedrock.prelude.bytestring]
BS.to_string [definition, in bedrock.prelude.bytestring]
BS.to_N_inj [abbreviation, in bedrock.prelude.bytestring_core]
BS.t_sind [definition, in bedrock.prelude.bytestring_core]
BS.t_rec [definition, in bedrock.prelude.bytestring_core]
BS.t_ind [definition, in bedrock.prelude.bytestring_core]
BS.t_rect [definition, in bedrock.prelude.bytestring_core]
build [abbreviation, in bedrock.prelude.avl]
Build_WrapN [abbreviation, in bedrock.prelude.wrap]
bytestring [library]
bytestring_parse_surj [instance, in bedrock.prelude.bytestring]
bytestring_print_surj [instance, in bedrock.prelude.bytestring]
bytestring_parse_inj [instance, in bedrock.prelude.bytestring]
bytestring_print_inj [instance, in bedrock.prelude.bytestring]
bytestring_print_parse_cancel [instance, in bedrock.prelude.bytestring]
bytestring_parse_print_cancel [instance, in bedrock.prelude.bytestring]
bytestring_countable [instance, in bedrock.prelude.bytestring]
bytestring_inhabited [instance, in bedrock.prelude.bytestring]
bytestring_eq_dec [instance, in bedrock.prelude.bytestring]
bytestring_core [library]
byte_of_N_surj [instance, in bedrock.prelude.bytestring]
byte_to_N_inj [instance, in bedrock.prelude.bytestring]
byte_countable [instance, in bedrock.prelude.bytestring]
byte_eq_dec [instance, in bedrock.prelude.bytestring]
byte_inhabited [instance, in bedrock.prelude.bytestring]
byte_cmp_spec [lemma, in bedrock.prelude.bytestring_core]
byte_to_N_inj [lemma, in bedrock.prelude.bytestring_core]
byte_cmp_refl [lemma, in bedrock.prelude.bytestring_core]
byte_compare [instance, in bedrock.prelude.bytestring_core]
byte_cmp [definition, in bedrock.prelude.bytestring_core]
byte_print [definition, in bedrock.prelude.bytestring_core]
byte_parse [definition, in bedrock.prelude.bytestring_core]
C
cancel_Build_WrapN_unwrapN [instance, in bedrock.prelude.wrap]cancel_unwrapN_Build_WrapN [instance, in bedrock.prelude.wrap]
cancel_MkwrapN [lemma, in bedrock.prelude.wrap]
cancel_unwrapN [lemma, in bedrock.prelude.wrap]
card_N [definition, in bedrock.prelude.finite]
Cbn [abbreviation, in bedrock.prelude.base]
char_parsec.MB [variable, in bedrock.prelude.parsec]
char_parsec.FM [variable, in bedrock.prelude.parsec]
char_parsec.MR [variable, in bedrock.prelude.parsec]
char_parsec.F [variable, in bedrock.prelude.parsec]
char_parsec [section, in bedrock.prelude.parsec]
check_canon_ok [abbreviation, in bedrock.prelude.avl]
check_canon_lem [abbreviation, in bedrock.prelude.avl]
check_canon [abbreviation, in bedrock.prelude.avl]
common [library]
compare [module, in bedrock.prelude.base]
compare [projection, in bedrock.prelude.base]
Compare [record, in bedrock.prelude.base]
compare [constructor, in bedrock.prelude.base]
Compare [inductive, in bedrock.prelude.base]
compare [section, in bedrock.prelude.base]
compare [section, in bedrock.prelude.compare]
compare [library]
compare_trans [projection, in bedrock.prelude.base]
compare_antisym [projection, in bedrock.prelude.base]
compare_lex [definition, in bedrock.prelude.compare]
compare_tag [definition, in bedrock.prelude.compare]
compare_ctor [definition, in bedrock.prelude.compare]
compare.compare [lemma, in bedrock.prelude.base]
compare.compare_spec [lemma, in bedrock.prelude.base]
compare.derived [section, in bedrock.prelude.base]
_ > _ [notation, in bedrock.prelude.base]
_ < _ [notation, in bedrock.prelude.base]
_ == _ [notation, in bedrock.prelude.base]
_ ?= _ [notation, in bedrock.prelude.base]
(?=) [notation, in bedrock.prelude.base]
compare.eq [definition, in bedrock.prelude.base]
compare.eq_equiv [instance, in bedrock.prelude.base]
compare.eq_dec [instance, in bedrock.prelude.base]
compare.ge [definition, in bedrock.prelude.base]
compare.ge_dec [instance, in bedrock.prelude.base]
compare.gt [definition, in bedrock.prelude.base]
compare.gt_dec [instance, in bedrock.prelude.base]
compare.le [definition, in bedrock.prelude.base]
compare.le_dec [instance, in bedrock.prelude.base]
compare.lt [definition, in bedrock.prelude.base]
compare.lt_trans [instance, in bedrock.prelude.base]
compare.lt_dec [instance, in bedrock.prelude.base]
compare.Notations [module, in bedrock.prelude.base]
(.>= _ ) (stdpp_scope) [notation, in bedrock.prelude.base]
( _ >=.) (stdpp_scope) [notation, in bedrock.prelude.base]
(>=@{ _ } ) (stdpp_scope) [notation, in bedrock.prelude.base]
(>=) (stdpp_scope) [notation, in bedrock.prelude.base]
_ >=@{ _ } _ (stdpp_scope) [notation, in bedrock.prelude.base]
_ >= _ (stdpp_scope) [notation, in bedrock.prelude.base]
(.> _ ) (stdpp_scope) [notation, in bedrock.prelude.base]
( _ >.) (stdpp_scope) [notation, in bedrock.prelude.base]
(>@{ _ } ) (stdpp_scope) [notation, in bedrock.prelude.base]
(>) (stdpp_scope) [notation, in bedrock.prelude.base]
_ >@{ _ } _ (stdpp_scope) [notation, in bedrock.prelude.base]
_ > _ (stdpp_scope) [notation, in bedrock.prelude.base]
(.<= _ ) (stdpp_scope) [notation, in bedrock.prelude.base]
( _ <=.) (stdpp_scope) [notation, in bedrock.prelude.base]
(<=@{ _ } ) (stdpp_scope) [notation, in bedrock.prelude.base]
(<=) (stdpp_scope) [notation, in bedrock.prelude.base]
_ <=@{ _ } _ (stdpp_scope) [notation, in bedrock.prelude.base]
_ <= _ (stdpp_scope) [notation, in bedrock.prelude.base]
(.< _ ) (stdpp_scope) [notation, in bedrock.prelude.base]
( _ <.) (stdpp_scope) [notation, in bedrock.prelude.base]
(<@{ _ } ) (stdpp_scope) [notation, in bedrock.prelude.base]
(<) (stdpp_scope) [notation, in bedrock.prelude.base]
_ <@{ _ } _ (stdpp_scope) [notation, in bedrock.prelude.base]
_ < _ (stdpp_scope) [notation, in bedrock.prelude.base]
(.?= _ ) (stdpp_scope) [notation, in bedrock.prelude.base]
( _ ?=.) (stdpp_scope) [notation, in bedrock.prelude.base]
(?=@{ _ } ) (stdpp_scope) [notation, in bedrock.prelude.base]
(?=) (stdpp_scope) [notation, in bedrock.prelude.base]
_ ?=@{ _ } _ (stdpp_scope) [notation, in bedrock.prelude.base]
_ ?= _ (stdpp_scope) [notation, in bedrock.prelude.base]
Comparison [record, in bedrock.prelude.base]
Compose [module, in bedrock.prelude.sts]
Compose.cancel_evt [projection, in bedrock.prelude.sts]
Compose.cancel_evt_asym [projection, in bedrock.prelude.sts]
Compose.Compose [section, in bedrock.prelude.sts]
Compose.Compose [section, in bedrock.prelude.sts]
Compose.compose_lts [definition, in bedrock.prelude.sts]
Compose.Compose.sf [variable, in bedrock.prelude.sts]
Compose.Compose.sf [variable, in bedrock.prelude.sts]
Compose.config [record, in bedrock.prelude.sts]
Compose.dual_sets_proper [instance, in bedrock.prelude.sts]
Compose.dual_sets_singletons [lemma, in bedrock.prelude.sts]
Compose.dual_sets [definition, in bedrock.prelude.sts]
Compose.eq_except [definition, in bedrock.prelude.sts]
Compose.external_event [projection, in bedrock.prelude.sts]
Compose.init_state [definition, in bedrock.prelude.sts]
Compose.inj_evt [projection, in bedrock.prelude.sts]
Compose.make [definition, in bedrock.prelude.sts]
Compose.name [projection, in bedrock.prelude.sts]
Compose.name_finite [projection, in bedrock.prelude.sts]
Compose.name_eq_dec [projection, in bedrock.prelude.sts]
Compose.State [definition, in bedrock.prelude.sts]
Compose.step_star_ext_lift_single [lemma, in bedrock.prelude.sts]
Compose.step_star_tau_lift [lemma, in bedrock.prelude.sts]
Compose.sts_name [projection, in bedrock.prelude.sts]
Compose._fam_sts [definition, in bedrock.prelude.sts]
constr_laws [lemma, in bedrock.prelude.lens]
constr_set_set [lemma, in bedrock.prelude.lens]
constr_set_view [lemma, in bedrock.prelude.lens]
constr_view_set [lemma, in bedrock.prelude.lens]
constr_view_over [lemma, in bedrock.prelude.lens]
cons_seqW' [lemma, in bedrock.prelude.wrap]
cons_seqW [lemma, in bedrock.prelude.wrap]
cons_seqN [lemma, in bedrock.prelude.list_numbers]
contraNN [lemma, in bedrock.prelude.bool]
countable [section, in bedrock.prelude.finite]
countable [library]
cpu [module, in bedrock.prelude.hw_types]
cpuT [abbreviation, in bedrock.prelude.hw_types]
cpu.count [definition, in bedrock.prelude.hw_types]
cpu.max [definition, in bedrock.prelude.hw_types]
D
decode_from_encode [definition, in bedrock.prelude.elpi.derive.countable]decode_N_is_inverse [lemma, in bedrock.prelude.finite]
decode_N_None_encode_N [lemma, in bedrock.prelude.finite]
decode_N_encode_N [lemma, in bedrock.prelude.finite]
decode_N_Some_encode_N [lemma, in bedrock.prelude.finite]
decode_N_nat [lemma, in bedrock.prelude.finite]
decode_nat_N [lemma, in bedrock.prelude.finite]
decode_encode_N [lemma, in bedrock.prelude.finite]
decode_N [definition, in bedrock.prelude.finite]
dec_stable_iff [lemma, in bedrock.prelude.base]
deps [definition, in bedrock.prelude.dummy]
dep_fn_insert_ne [abbreviation, in bedrock.prelude.functions]
dep_fn_insert_eq [abbreviation, in bedrock.prelude.functions]
dep_fn_insert_exchange_fun [lemma, in bedrock.prelude.functions]
dep_fn_insert_set_set_fun [lemma, in bedrock.prelude.functions]
dep_fn_insert_set_view_fun [lemma, in bedrock.prelude.functions]
dep_fn_insert_exchange [lemma, in bedrock.prelude.functions]
dep_fn_insert_set_set [lemma, in bedrock.prelude.functions]
dep_fn_insert_set_view [lemma, in bedrock.prelude.functions]
dep_fn_insert_view_set_ne [lemma, in bedrock.prelude.functions]
dep_fn_insert_view_set' [lemma, in bedrock.prelude.functions]
dep_fn_insert_view_set [lemma, in bedrock.prelude.functions]
dep_fn_insert [definition, in bedrock.prelude.functions]
dep_fn_insert.T [variable, in bedrock.prelude.functions]
dep_fn_insert.A [variable, in bedrock.prelude.functions]
dep_fn_insert [section, in bedrock.prelude.functions]
derive [library]
derive_test [library]
DerivingTest [module, in bedrock.prelude.elpi.derive_test]
DerivingTest.A [constructor, in bedrock.prelude.elpi.derive_test]
DerivingTest.B [constructor, in bedrock.prelude.elpi.derive_test]
DerivingTest.C [constructor, in bedrock.prelude.elpi.derive_test]
DerivingTest.t [definition, in bedrock.prelude.elpi.derive_test]
DerivingTest.t_countable [definition, in bedrock.prelude.elpi.derive_test]
DerivingTest.t_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
DerivingTest.Unnamed_thm1 [definition, in bedrock.prelude.elpi.derive_test]
DerivingTest.Unnamed_thm0 [definition, in bedrock.prelude.elpi.derive_test]
DerivingTest.Unnamed_thm [definition, in bedrock.prelude.elpi.derive_test]
DerivingTest._t [inductive, in bedrock.prelude.elpi.derive_test]
Deriving2Test [module, in bedrock.prelude.elpi.derive_test]
Deriving2Test.A [constructor, in bedrock.prelude.elpi.derive_test]
Deriving2Test.B [constructor, in bedrock.prelude.elpi.derive_test]
Deriving2Test.C [constructor, in bedrock.prelude.elpi.derive_test]
Deriving2Test.D [constructor, in bedrock.prelude.elpi.derive_test]
Deriving2Test.E [constructor, in bedrock.prelude.elpi.derive_test]
Deriving2Test.F [constructor, in bedrock.prelude.elpi.derive_test]
Deriving2Test.G [constructor, in bedrock.prelude.elpi.derive_test]
Deriving2Test.H [constructor, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.test [section, in bedrock.prelude.elpi.derive_test]
Deriving2Test.test.x [variable, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_finite2 [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_finite [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_inhabited [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2 [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_finite [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_inhabited [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3 [inductive, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_finite [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_inhabited [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.Unnamed_thm1 [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.Unnamed_thm0 [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test.Unnamed_thm [definition, in bedrock.prelude.elpi.derive_test]
Deriving2Test._t2 [inductive, in bedrock.prelude.elpi.derive_test]
Deriving2Test._t [inductive, in bedrock.prelude.elpi.derive_test]
difference_map_disjoint [lemma, in bedrock.prelude.fin_maps]
digit [definition, in bedrock.prelude.parsec]
Disjoint [abbreviation, in bedrock.prelude.list]
disjoint_cons_r [lemma, in bedrock.prelude.list]
dom_seqZ_L [lemma, in bedrock.prelude.fin_map_dom]
dom_seqZ [lemma, in bedrock.prelude.fin_map_dom]
dom_map_seqZ.HF [variable, in bedrock.prelude.fin_map_dom]
dom_map_seqZ.HP [variable, in bedrock.prelude.fin_map_dom]
dom_map_seqZ.HE [variable, in bedrock.prelude.fin_map_dom]
dom_map_seqZ.HL [variable, in bedrock.prelude.fin_map_dom]
dom_map_seqZ [section, in bedrock.prelude.fin_map_dom]
dropN [definition, in bedrock.prelude.list_numbers]
dropN_sliceZ [lemma, in bedrock.prelude.list_numbers]
dropN_congr [lemma, in bedrock.prelude.list_numbers]
dropN_insertN_lt [lemma, in bedrock.prelude.list_numbers]
dropN_insertN_ge [lemma, in bedrock.prelude.list_numbers]
dropN_lookupN [lemma, in bedrock.prelude.list_numbers]
dropN_resizeN_le [lemma, in bedrock.prelude.list_numbers]
dropN_resizeN_plus [lemma, in bedrock.prelude.list_numbers]
dropN_takeN [lemma, in bedrock.prelude.list_numbers]
dropN_app [lemma, in bedrock.prelude.list_numbers]
dropN_cons_succ [lemma, in bedrock.prelude.list_numbers]
dropN_nil [lemma, in bedrock.prelude.list_numbers]
dropN_dropN [lemma, in bedrock.prelude.list_numbers]
dropN_tail [lemma, in bedrock.prelude.list_numbers]
dropN_one [lemma, in bedrock.prelude.list_numbers]
dropN_zero [lemma, in bedrock.prelude.list_numbers]
dropN_lengthN [lemma, in bedrock.prelude.list_numbers]
dropN_replicateN_succ [lemma, in bedrock.prelude.list_numbers]
dropN_replicateN_plus [lemma, in bedrock.prelude.list_numbers]
dropN_replicateN [lemma, in bedrock.prelude.list_numbers]
dropN_seqN_cons [lemma, in bedrock.prelude.list_numbers]
dropN_seqN [lemma, in bedrock.prelude.list_numbers]
dummy [library]
E
EdgeSig [constructor, in bedrock.prelude.interrupts]elements_set_seq [lemma, in bedrock.prelude.fin_sets]
elements_leibniz_inj [instance, in bedrock.prelude.fin_sets]
elements_set_equiv_L [lemma, in bedrock.prelude.fin_sets]
elements_perm [instance, in bedrock.prelude.fin_sets]
elements_mono [instance, in bedrock.prelude.fin_sets]
elements_set_equiv_1 [lemma, in bedrock.prelude.fin_sets]
elements_inj [instance, in bedrock.prelude.fin_sets]
elem_of_map_to_list_dom [lemma, in bedrock.prelude.fin_map_dom]
elem_of_list_fmap_ap [lemma, in bedrock.prelude.list]
elem_of_list_ap [lemma, in bedrock.prelude.list]
elem_of_zip [lemma, in bedrock.prelude.list]
elem_of_rangeZ [lemma, in bedrock.prelude.list_numbers]
elem_of_replicateN [lemma, in bedrock.prelude.list_numbers]
elem_of_seqN [lemma, in bedrock.prelude.list_numbers]
elem_of_set_rangeZ [lemma, in bedrock.prelude.fin_sets]
elem_of_set_concat_map [lemma, in bedrock.prelude.fin_sets]
elem_of_gset_bind [lemma, in bedrock.prelude.gmap]
elem_of_app_fmap_enum_l [lemma, in bedrock.prelude.finite]
elem_of_finite_preimage_set [lemma, in bedrock.prelude.finite]
elem_of_finite_preimage [lemma, in bedrock.prelude.finite]
elem_of_filter_enum [lemma, in bedrock.prelude.finite]
elem_of_enum' [lemma, in bedrock.prelude.finite]
elimT [lemma, in bedrock.prelude.bool]
encode_decode_N [lemma, in bedrock.prelude.finite]
encode_N_lt_card_N [lemma, in bedrock.prelude.finite]
encode_N_nat [lemma, in bedrock.prelude.finite]
encode_nat_N [lemma, in bedrock.prelude.finite]
encode_N_inj [instance, in bedrock.prelude.finite]
encode_N [definition, in bedrock.prelude.finite]
enc_finite_N [definition, in bedrock.prelude.finite]
enc_finite_N.to_of_N [variable, in bedrock.prelude.finite]
enc_finite_N.to_N_c [variable, in bedrock.prelude.finite]
enc_finite_N.of_to_N [variable, in bedrock.prelude.finite]
enc_finite_N.c [variable, in bedrock.prelude.finite]
enc_finite_N.of_N [variable, in bedrock.prelude.finite]
enc_finite_N.to_N [variable, in bedrock.prelude.finite]
enc_finite_N [section, in bedrock.prelude.finite]
enc_finite_enum [lemma, in bedrock.prelude.finite]
enc_finite.to_of_nat [variable, in bedrock.prelude.finite]
enc_finite.to_nat_c [variable, in bedrock.prelude.finite]
enc_finite.of_to_nat [variable, in bedrock.prelude.finite]
enc_finite.c [variable, in bedrock.prelude.finite]
enc_finite.of_nat [variable, in bedrock.prelude.finite]
enc_finite.to_nat [variable, in bedrock.prelude.finite]
enc_finite [section, in bedrock.prelude.finite]
enum_lookup_encode_N [lemma, in bedrock.prelude.finite]
enum_lookup_encode_nat [lemma, in bedrock.prelude.finite]
eqdec_type.t_eq_dec [instance, in bedrock.prelude.finite]
eqdec_type.t [axiom, in bedrock.prelude.finite]
eqdec_type [module, in bedrock.prelude.finite]
Eq_Gt_discr [definition, in bedrock.prelude.numbers]
Eq_Lt_discr [definition, in bedrock.prelude.numbers]
eq_dec [library]
Error [module, in bedrock.prelude.error]
ERROR [module, in bedrock.prelude.error]
error [library]
Error.exc [definition, in bedrock.prelude.error]
ERROR.exc [instance, in bedrock.prelude.error]
Error.t [definition, in bedrock.prelude.error]
ERROR.t [axiom, in bedrock.prelude.error]
Evaluate [abbreviation, in bedrock.prelude.base]
exact_char [definition, in bedrock.prelude.parsec]
exact_bs [definition, in bedrock.prelude.parsec]
F
fin [module, in bedrock.prelude.fin]fin [library]
find_any_ok [abbreviation, in bedrock.prelude.avl]
find_any [abbreviation, in bedrock.prelude.avl]
finite [section, in bedrock.prelude.finite]
finite [library]
finite [library]
FiniteTest [module, in bedrock.prelude.elpi.derive_test]
FiniteTest.A [constructor, in bedrock.prelude.elpi.derive_test]
FiniteTest.B [constructor, in bedrock.prelude.elpi.derive_test]
FiniteTest.C [constructor, in bedrock.prelude.elpi.derive_test]
FiniteTest.D [constructor, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature [module, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature [inductive, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature_to_N_inj [instance, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature_finite [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature.t [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature.to_N [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature.t_finite [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.feature.t_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.Unnamed_thm1 [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.Unnamed_thm0 [definition, in bedrock.prelude.elpi.derive_test]
FiniteTest.Unnamed_thm [definition, in bedrock.prelude.elpi.derive_test]
finite_bits [module, in bedrock.prelude.finite]
finite_bits_aux.to_bits_inv_singleton_ne_Z [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bits_inv_singleton_Z [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bits_inv_singleton_ne [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bits_inv_singleton [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_of_bits [lemma, in bedrock.prelude.finite]
finite_bits_aux.N_testbit_mask_top_to_bit [lemma, in bedrock.prelude.finite]
finite_bits_aux.N_testbit_to_bits [lemma, in bedrock.prelude.finite]
finite_bits_aux.elem_of_masked [lemma, in bedrock.prelude.finite]
finite_bits_aux.masked_opt_top [lemma, in bedrock.prelude.finite]
finite_bits_aux.masked_top [lemma, in bedrock.prelude.finite]
finite_bits_aux.mask_top [definition, in bedrock.prelude.finite]
finite_bits_aux.masked_opt_empty [lemma, in bedrock.prelude.finite]
finite_bits_aux.masked_empty [lemma, in bedrock.prelude.finite]
finite_bits_aux.masked_opt_0 [lemma, in bedrock.prelude.finite]
finite_bits_aux.masked_0 [lemma, in bedrock.prelude.finite]
finite_bits_aux.masked_opt [definition, in bedrock.prelude.finite]
finite_bits_aux.masked [definition, in bedrock.prelude.finite]
finite_bits_aux.of_bits_surj [instance, in bedrock.prelude.finite]
finite_bits_aux.to_bits_inj [instance, in bedrock.prelude.finite]
finite_bits_aux.of_to_bits_cancel [instance, in bedrock.prelude.finite]
finite_bits_aux.of_bits_singleton [lemma, in bedrock.prelude.finite]
finite_bits_aux.of_to_bits [lemma, in bedrock.prelude.finite]
finite_bits_aux.of_bits_setbit [lemma, in bedrock.prelude.finite]
finite_bits_aux.BT_to_bit_inj.Hinj [variable, in bedrock.prelude.finite]
finite_bits_aux.BT_to_bit_inj [section, in bedrock.prelude.finite]
finite_bits_aux.to_bits_intersection [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bits_intersection_singleton [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bitmask_land_neq [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bits_union [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bits_union_singleton [lemma, in bedrock.prelude.finite]
finite_bits_aux.setbit_in_idemp [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bits_union_singleton_aux [lemma, in bedrock.prelude.finite]
finite_bits_aux.internal.to_bits_is_comm [lemma, in bedrock.prelude.finite]
finite_bits_aux.internal.to_bits_comm [definition, in bedrock.prelude.finite]
finite_bits_aux.internal.to_bits_is_alt [lemma, in bedrock.prelude.finite]
finite_bits_aux.internal.to_bits_alt [definition, in bedrock.prelude.finite]
finite_bits_aux.internal [module, in bedrock.prelude.finite]
finite_bits_aux.to_bits_singleton [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bits_empty [lemma, in bedrock.prelude.finite]
finite_bits_aux.to_bits [definition, in bedrock.prelude.finite]
finite_bits_aux.of_bits_and [lemma, in bedrock.prelude.finite]
finite_bits_aux.of_bits_or [lemma, in bedrock.prelude.finite]
finite_bits_aux.of_bits_0 [lemma, in bedrock.prelude.finite]
finite_bits_aux.set_unfold_elem_of_to_list [instance, in bedrock.prelude.finite]
finite_bits_aux.elem_of_of_bits [lemma, in bedrock.prelude.finite]
finite_bits_aux.of_bits [definition, in bedrock.prelude.finite]
finite_bits_aux.topset_t [instance, in bedrock.prelude.finite]
finite_bits_aux.top_t [instance, in bedrock.prelude.finite]
finite_bits_aux.t [definition, in bedrock.prelude.finite]
finite_bits_aux [module, in bedrock.prelude.finite]
finite_bitmask_type_intf [module, in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_list_setbit [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.filter_setbit [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.filter_setbit' [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_testbit_to_bitmask_inj [instance, in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_to_bitmask_inj [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_testbit_setbit_inj [instance, in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_setbit_inj [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_bit_inj.Hinj [variable, in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_bit_inj [section, in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_to_bitmask_eq [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_to_bitmask [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_setbit [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.setbit_is_alt [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.setbit_0 [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.setbit_alt [abbreviation, in bedrock.prelude.finite]
finite_bitmask_type_mixin.setbit [definition, in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_to_list_and [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_to_list_or [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_to_list_0 [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_list_0 [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_elem_of_to_list [instance, in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_to_list [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_list [definition, in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_list_aux [definition, in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_filter_0 [instance, in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_filter_land [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_filter_lor [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.filter_0 [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_filter [instance, in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_filter [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.filter [definition, in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_testbit_land [instance, in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_testbit_lor [instance, in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_land [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_lor [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_0 [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit [definition, in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_bitmask_setbit [lemma, in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_bitmask [definition, in bedrock.prelude.finite]
finite_bitmask_type_mixin [module, in bedrock.prelude.finite]
finite_type_intf [module, in bedrock.prelude.finite]
finite_type_mixin.to_N_lt_card_N [lemma, in bedrock.prelude.finite]
finite_type_mixin.to_of_N [lemma, in bedrock.prelude.finite]
finite_type_mixin.of_to_N [lemma, in bedrock.prelude.finite]
finite_type_mixin.of_N [definition, in bedrock.prelude.finite]
finite_type_mixin.to_N [definition, in bedrock.prelude.finite]
finite_type_mixin.t_countable [definition, in bedrock.prelude.finite]
finite_type_mixin [module, in bedrock.prelude.finite]
finite_encoded_type_mixin.to_of_N [lemma, in bedrock.prelude.finite]
finite_encoded_type_mixin.of_to_N [lemma, in bedrock.prelude.finite]
finite_encoded_type_mixin.of_N [definition, in bedrock.prelude.finite]
finite_encoded_type_mixin [module, in bedrock.prelude.finite]
finite_encoded_type.to_N [axiom, in bedrock.prelude.finite]
finite_encoded_type [module, in bedrock.prelude.finite]
finite_type.t_finite [instance, in bedrock.prelude.finite]
finite_type [module, in bedrock.prelude.finite]
finite_decode_N_lt [lemma, in bedrock.prelude.finite]
finite_decode_N_unfold [lemma, in bedrock.prelude.finite]
finite_decode_N_unfold' [lemma, in bedrock.prelude.finite]
finite_decode_nat_lt [lemma, in bedrock.prelude.finite]
finite_decode_nat_unfold [lemma, in bedrock.prelude.finite]
finite_preimage_gset [abbreviation, in bedrock.prelude.finite]
finite_preimage_set_params [instance, in bedrock.prelude.finite]
finite_preimage_set_inj_singleton_L [lemma, in bedrock.prelude.finite]
finite_preimage_set_singleton_L [lemma, in bedrock.prelude.finite]
finite_preimage_set_union_L [lemma, in bedrock.prelude.finite]
finite_preimage_set_empty_L [lemma, in bedrock.prelude.finite]
finite_preimage_set.finite_preimage_set_leibniz [section, in bedrock.prelude.finite]
finite_preimage_set_inj_singleton [lemma, in bedrock.prelude.finite]
finite_preimage_set_singleton [lemma, in bedrock.prelude.finite]
finite_preimage_set_union [lemma, in bedrock.prelude.finite]
finite_preimage_set_mono [instance, in bedrock.prelude.finite]
finite_preimage_set_proper [instance, in bedrock.prelude.finite]
finite_preimage_set_empty [lemma, in bedrock.prelude.finite]
finite_preimage_set [definition, in bedrock.prelude.finite]
finite_preimage_set [section, in bedrock.prelude.finite]
finite_inverse_inj_Some_equiv [lemma, in bedrock.prelude.finite]
finite_inverse_inj_cancel [lemma, in bedrock.prelude.finite]
finite_preimage.finite_preimage_inj.Hinj [variable, in bedrock.prelude.finite]
finite_preimage.finite_preimage_inj [section, in bedrock.prelude.finite]
finite_inverse_None_equiv [lemma, in bedrock.prelude.finite]
finite_inverse_is_Some [lemma, in bedrock.prelude.finite]
finite_inverse_Some_inv [lemma, in bedrock.prelude.finite]
finite_inverse [definition, in bedrock.prelude.finite]
finite_preimage_inj_singleton [lemma, in bedrock.prelude.finite]
finite_preimage [definition, in bedrock.prelude.finite]
finite_preimage [section, in bedrock.prelude.finite]
finite_stdlib [section, in bedrock.prelude.finite]
finite_type [library]
finite_prod [library]
finset [section, in bedrock.prelude.fin_sets]
finset.elements [section, in bedrock.prelude.fin_sets]
finset.elements.elements_leibniz [section, in bedrock.prelude.fin_sets]
fin_map_dom.A [variable, in bedrock.prelude.fin_map_dom]
fin_map_dom [section, in bedrock.prelude.fin_map_dom]
fin_prod.lookup_ext [lemma, in bedrock.prelude.finite_prod]
fin_prod.lookup_update_ne [lemma, in bedrock.prelude.finite_prod]
fin_prod.lookup_update_eq [lemma, in bedrock.prelude.finite_prod]
fin_prod.fmapO_None [lemma, in bedrock.prelude.finite_prod]
fin_prod.fmapO_Some [lemma, in bedrock.prelude.finite_prod]
fin_prod.lookup_fmap [lemma, in bedrock.prelude.finite_prod]
fin_prod.lookup_unfold [lemma, in bedrock.prelude.finite_prod]
fin_prod.update [definition, in bedrock.prelude.finite_prod]
fin_prod.fmapO [definition, in bedrock.prelude.finite_prod]
fin_prod.fmap [definition, in bedrock.prelude.finite_prod]
fin_prod.lookup [definition, in bedrock.prelude.finite_prod]
fin_prod.to_list [definition, in bedrock.prelude.finite_prod]
fin_prod.with_finite [section, in bedrock.prelude.finite_prod]
fin_prod.internal.fmapO'_None [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.fmapO'_Some_1 [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.fmapO'_Some [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.lookup_fmap' [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_fg.ns [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_fg.B [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_fg.A [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_fg [section, in bedrock.prelude.finite_prod]
fin_prod.internal.lookup'_ext [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.lookup_update'_ne [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.lookup_update'_eq [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.lookup'_elem_of_Some [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_eq_dec.ns [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_eq_dec.A [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_eq_dec [section, in bedrock.prelude.finite_prod]
fin_prod.internal.to_list'_cons [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.to_list'_nil [lemma, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_type.A [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_type.name [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_type [section, in bedrock.prelude.finite_prod]
fin_prod.internal.update' [definition, in bedrock.prelude.finite_prod]
fin_prod.internal.lookup' [definition, in bedrock.prelude.finite_prod]
fin_prod.internal.with_eq_dec.A [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.with_eq_dec [section, in bedrock.prelude.finite_prod]
fin_prod.internal.fmapO' [definition, in bedrock.prelude.finite_prod]
fin_prod.internal.fmap' [definition, in bedrock.prelude.finite_prod]
fin_prod.internal.with_fg.B [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.with_fg.A [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.with_fg.name [variable, in bedrock.prelude.finite_prod]
fin_prod.internal.with_fg [section, in bedrock.prelude.finite_prod]
fin_prod.internal.to_list' [definition, in bedrock.prelude.finite_prod]
fin_prod.internal [module, in bedrock.prelude.finite_prod]
fin_prod [module, in bedrock.prelude.finite_prod]
fin_set_pairwise_disjoint_dec [instance, in bedrock.prelude.fin_sets]
fin_set [section, in bedrock.prelude.fin_sets]
fin_maps.A [variable, in bedrock.prelude.fin_maps]
fin_maps [section, in bedrock.prelude.fin_maps]
fin_fun_eq_refl_transport [lemma, in bedrock.prelude.finite]
fin_fun_eq_refl [lemma, in bedrock.prelude.finite]
fin_fun_decide_True_pi [lemma, in bedrock.prelude.finite]
fin_fun_eq_pi [instance, in bedrock.prelude.finite]
fin_fun_eq_dec [instance, in bedrock.prelude.finite]
fin_fun_eq_dec [section, in bedrock.prelude.finite]
fin_sets [library]
fin_map_dom [library]
fin_maps [library]
fin.decode [definition, in bedrock.prelude.fin]
fin.elem_of_seq [lemma, in bedrock.prelude.fin]
fin.enum_unfold [lemma, in bedrock.prelude.fin]
fin.is_succ [lemma, in bedrock.prelude.fin]
fin.is_zero [lemma, in bedrock.prelude.fin]
fin.is_mk [lemma, in bedrock.prelude.fin]
fin.lit [abbreviation, in bedrock.prelude.fin]
fin.mk [definition, in bedrock.prelude.fin]
fin.of_to_idx_fin_cancel [lemma, in bedrock.prelude.fin]
fin.of_idx_fin [abbreviation, in bedrock.prelude.fin]
fin.of_idx_fin' [definition, in bedrock.prelude.fin]
fin.of_to_N [lemma, in bedrock.prelude.fin]
fin.of_to_N' [lemma, in bedrock.prelude.fin]
fin.of_nat [definition, in bedrock.prelude.fin]
fin.of_N [definition, in bedrock.prelude.fin]
fin.of_nat' [definition, in bedrock.prelude.fin]
fin.of_N' [definition, in bedrock.prelude.fin]
fin.proj1_sig_of_N [lemma, in bedrock.prelude.fin]
fin.seq [definition, in bedrock.prelude.fin]
fin.seq_lookupN [lemma, in bedrock.prelude.fin]
fin.seq_NoDup [lemma, in bedrock.prelude.fin]
fin.seq_len [lemma, in bedrock.prelude.fin]
fin.seq_lenN [lemma, in bedrock.prelude.fin]
fin.succ [definition, in bedrock.prelude.fin]
fin.t [definition, in bedrock.prelude.fin]
fin.to_of_idx_fin_cancel [lemma, in bedrock.prelude.fin]
fin.to_idx_fin [abbreviation, in bedrock.prelude.fin]
fin.to_idx_fin' [definition, in bedrock.prelude.fin]
fin.to_N_inj [instance, in bedrock.prelude.fin]
fin.to_of_N_gt [lemma, in bedrock.prelude.fin]
fin.to_of_N [lemma, in bedrock.prelude.fin]
fin.to_of_N_gt' [lemma, in bedrock.prelude.fin]
fin.to_of_N' [lemma, in bedrock.prelude.fin]
fin.to_N_lt [lemma, in bedrock.prelude.fin]
fin.to_N [definition, in bedrock.prelude.fin]
fin.t_rect [lemma, in bedrock.prelude.fin]
fin.t_sig_rect [lemma, in bedrock.prelude.fin]
fin.t_finite [instance, in bedrock.prelude.fin]
fin.t_gt_inhabited [lemma, in bedrock.prelude.fin]
fin.t_pos_inhabited [instance, in bedrock.prelude.fin]
fin.t_countable [instance, in bedrock.prelude.fin]
fin.t_eq_dec [instance, in bedrock.prelude.fin]
fin.t_eq [definition, in bedrock.prelude.fin]
fin.t_inv [lemma, in bedrock.prelude.fin]
fin.t_0_inv [lemma, in bedrock.prelude.fin]
fin.Unnamed_thm [definition, in bedrock.prelude.fin]
fin.Unnamed_thm [definition, in bedrock.prelude.fin]
fin.weaken [abbreviation, in bedrock.prelude.fin]
fin.weaken_bool_decide [definition, in bedrock.prelude.fin]
fin.weaken' [definition, in bedrock.prelude.fin]
fin.zero [definition, in bedrock.prelude.fin]
flip_app_assoc [instance, in bedrock.prelude.base]
flip_app_right_id [instance, in bedrock.prelude.base]
flip_app_left_id [instance, in bedrock.prelude.base]
flip_app.A [variable, in bedrock.prelude.base]
flip_app [section, in bedrock.prelude.base]
flip_assoc [lemma, in bedrock.prelude.base]
flip2 [definition, in bedrock.prelude.base]
FMapExtra [module, in bedrock.prelude.avl]
FMapExtra.LEIBNIZ_EQ.eqL [axiom, in bedrock.prelude.avl]
FMapExtra.LEIBNIZ_EQ [module, in bedrock.prelude.avl]
FMapExtra.MAP [module, in bedrock.prelude.avl]
FMapExtra.MAP.bst [record, in bedrock.prelude.avl]
FMapExtra.MAP.is_bst [projection, in bedrock.prelude.avl]
FMapExtra.MAP.Raw [module, in bedrock.prelude.avl]
FMapExtra.MAP.this [projection, in bedrock.prelude.avl]
FMapExtra.MIXIN [module, in bedrock.prelude.avl]
FMapExtra.MIXIN_LEIBNIZ.find_any_ok [lemma, in bedrock.prelude.avl]
FMapExtra.MIXIN_LEIBNIZ.find_any [definition, in bedrock.prelude.avl]
FMapExtra.MIXIN_LEIBNIZ.map_to_list_elements [lemma, in bedrock.prelude.avl]
FMapExtra.MIXIN_LEIBNIZ.K [abbreviation, in bedrock.prelude.avl]
FMapExtra.MIXIN_LEIBNIZ [module, in bedrock.prelude.avl]
FMapExtra.MIXIN.build [definition, in bedrock.prelude.avl]
FMapExtra.MIXIN.canon [section, in bedrock.prelude.avl]
FMapExtra.MIXIN.canon.A [variable, in bedrock.prelude.avl]
FMapExtra.MIXIN.check_canon_ok [lemma, in bedrock.prelude.avl]
FMapExtra.MIXIN.check_canonP [lemma, in bedrock.prelude.avl]
FMapExtra.MIXIN.check_canon [definition, in bedrock.prelude.avl]
FMapExtra.MIXIN.from_raw [definition, in bedrock.prelude.avl]
FMapExtra.MIXIN.from_raw_or [definition, in bedrock.prelude.avl]
FMapExtra.MIXIN.K [abbreviation, in bedrock.prelude.avl]
FMapExtra.MIXIN.key_eq_dec [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.key_lt_dec [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.M [abbreviation, in bedrock.prelude.avl]
FMapExtra.MIXIN.M [abbreviation, in bedrock.prelude.avl]
FMapExtra.MIXIN.map [section, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_canon [definition, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_merge [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_map [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_partial_alter [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_singleton [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_mapfold [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_lookup [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_delete [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_insert [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.map_empty [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.map.A [variable, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw [section, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_omap [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_merge [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_map [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_singleton [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_mapfold [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_lookup [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_delete [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_insert [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_empty [instance, in bedrock.prelude.avl]
FMapExtra.MIXIN.raw.A [variable, in bedrock.prelude.avl]
FMapExtra.RAW [module, in bedrock.prelude.avl]
FMapExtra.RAW.BSLeaf [constructor, in bedrock.prelude.avl]
FMapExtra.RAW.BSNode [constructor, in bedrock.prelude.avl]
FMapExtra.RAW.bst [inductive, in bedrock.prelude.avl]
FMapExtra.RAW.bst [section, in bedrock.prelude.avl]
FMapExtra.RAW.bst_sind [definition, in bedrock.prelude.avl]
FMapExtra.RAW.bst_ind [definition, in bedrock.prelude.avl]
FMapExtra.RAW.bst.elt [variable, in bedrock.prelude.avl]
FMapExtra.RAW.gt_tree [definition, in bedrock.prelude.avl]
FMapExtra.RAW.In [inductive, in bedrock.prelude.avl]
FMapExtra.RAW.InLeft [constructor, in bedrock.prelude.avl]
FMapExtra.RAW.InRight [constructor, in bedrock.prelude.avl]
FMapExtra.RAW.InRoot [constructor, in bedrock.prelude.avl]
FMapExtra.RAW.In_sind [definition, in bedrock.prelude.avl]
FMapExtra.RAW.In_ind [definition, in bedrock.prelude.avl]
FMapExtra.RAW.key [abbreviation, in bedrock.prelude.avl]
FMapExtra.RAW.Leaf [constructor, in bedrock.prelude.avl]
FMapExtra.RAW.lt_tree [definition, in bedrock.prelude.avl]
FMapExtra.RAW.map [axiom, in bedrock.prelude.avl]
FMapExtra.RAW.mapi [axiom, in bedrock.prelude.avl]
FMapExtra.RAW.map_option [axiom, in bedrock.prelude.avl]
FMapExtra.RAW.map2 [axiom, in bedrock.prelude.avl]
FMapExtra.RAW.map2_opt [axiom, in bedrock.prelude.avl]
FMapExtra.RAW.Node [constructor, in bedrock.prelude.avl]
FMapExtra.RAW.ops [section, in bedrock.prelude.avl]
FMapExtra.RAW.ops.add [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.bal [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.cardinal [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.concat [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.create [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.elements [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.elements_aux [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.elt [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.empty [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.equal [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.find [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.fold [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.height [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.is_empty [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.join [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.mem [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.merge [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.remove [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.remove_min [variable, in bedrock.prelude.avl]
FMapExtra.RAW.ops.split [variable, in bedrock.prelude.avl]
FMapExtra.RAW.Proofs [module, in bedrock.prelude.avl]
FMapExtra.RAW.Proofs.MX [module, in bedrock.prelude.avl]
FMapExtra.RAW.t [abbreviation, in bedrock.prelude.avl]
FMapExtra.RAW.t [abbreviation, in bedrock.prelude.avl]
FMapExtra.RAW.t [abbreviation, in bedrock.prelude.avl]
FMapExtra.RAW.tree [inductive, in bedrock.prelude.avl]
FMapExtra.RAW.tree_sind [definition, in bedrock.prelude.avl]
FMapExtra.RAW.tree_rec [definition, in bedrock.prelude.avl]
FMapExtra.RAW.tree_ind [definition, in bedrock.prelude.avl]
FMapExtra.RAW.tree_rect [definition, in bedrock.prelude.avl]
FMapExtra.RAW.triple [record, in bedrock.prelude.avl]
FMapExtra.RAW.t_right [projection, in bedrock.prelude.avl]
FMapExtra.RAW.t_opt [projection, in bedrock.prelude.avl]
FMapExtra.RAW.t_left [projection, in bedrock.prelude.avl]
fmap_ext_in [lemma, in bedrock.prelude.list]
fmap_S_seqN [lemma, in bedrock.prelude.list_numbers]
fmap_add_seqN_0 [lemma, in bedrock.prelude.list_numbers]
fmap_add_seqN [lemma, in bedrock.prelude.list_numbers]
fmap_dropN [lemma, in bedrock.prelude.list_numbers]
fmap_lengthN [lemma, in bedrock.prelude.list_numbers]
fmap_add_seq_0 [lemma, in bedrock.prelude.list_numbers]
fn_lookup_total_unfold [lemma, in bedrock.prelude.functions]
fn_lookup_total [instance, in bedrock.prelude.functions]
foldl_left [lemma, in bedrock.prelude.list]
foldl_rev [lemma, in bedrock.prelude.list]
foldr_rev [lemma, in bedrock.prelude.list]
foldr_cons [lemma, in bedrock.prelude.list]
fold_left_cons [lemma, in bedrock.prelude.avl]
ForallT [inductive, in bedrock.prelude.list]
ForallT_true [definition, in bedrock.prelude.list]
ForallT_sind [definition, in bedrock.prelude.list]
ForallT_rec [definition, in bedrock.prelude.list]
ForallT_ind [definition, in bedrock.prelude.list]
ForallT_rect [definition, in bedrock.prelude.list]
ForallT_cons [constructor, in bedrock.prelude.list]
ForallT_nil [constructor, in bedrock.prelude.list]
Forall_fmap_fmap [lemma, in bedrock.prelude.list]
Forall_fmap_fmap_1 [lemma, in bedrock.prelude.list]
Forall_seqN [lemma, in bedrock.prelude.list_numbers]
Forall2_symmetric_strong [lemma, in bedrock.prelude.list]
force_some [definition, in bedrock.prelude.option]
from_raw [abbreviation, in bedrock.prelude.avl]
from_raw_or [abbreviation, in bedrock.prelude.avl]
from_forall_named_binder [instance, in bedrock.prelude.named_binder]
functions [library]
funext [library]
funext_equiv [lemma, in bedrock.prelude.axioms.funext]
G
get_range_bitsN_bounded_elim' [lemma, in bedrock.prelude.bitsN]get_range_bitsN_bounded_elim [lemma, in bedrock.prelude.bitsN]
get_range_bitsN.get_range_bitsN_bounded_elim.from [variable, in bedrock.prelude.bitsN]
get_range_bitsN.get_range_bitsN_bounded_elim.n [variable, in bedrock.prelude.bitsN]
get_range_bitsN.get_range_bitsN_bounded_elim.count [variable, in bedrock.prelude.bitsN]
get_range_bitsN.get_range_bitsN_bounded_elim.of_N [variable, in bedrock.prelude.bitsN]
get_range_bitsN.get_range_bitsN_bounded_elim.X [variable, in bedrock.prelude.bitsN]
get_range_bitsN.get_range_bitsN_bounded_elim [section, in bedrock.prelude.bitsN]
get_range_bits_fin [definition, in bedrock.prelude.bitsN]
get_range_bitsN_bounded [lemma, in bedrock.prelude.bitsN]
get_range_bitsN_1_bool_decide_eq [lemma, in bedrock.prelude.bitsN]
get_range_bitsN_1_eq [lemma, in bedrock.prelude.bitsN]
get_range_bitsN_eq [lemma, in bedrock.prelude.bitsN]
get_range_bitsN [section, in bedrock.prelude.bitsN]
get_range_bitsN [definition, in bedrock.prelude.bitsN]
get_some [definition, in bedrock.prelude.option]
gmap [library]
gset_bind_singleton [lemma, in bedrock.prelude.gmap]
gset_bind_union [lemma, in bedrock.prelude.gmap]
gset_bind_empty [lemma, in bedrock.prelude.gmap]
gset_bind [definition, in bedrock.prelude.gmap]
gset_bind [section, in bedrock.prelude.gmap]
gset_concat_map [abbreviation, in bedrock.prelude.gmap]
gset_map [abbreviation, in bedrock.prelude.gmap]
gset_eq [lemma, in bedrock.prelude.gmap]
Gt_Lt_discr [definition, in bedrock.prelude.numbers]
Gt_Eq_discr [definition, in bedrock.prelude.numbers]
GuestInt [constructor, in bedrock.prelude.interrupts]
H
head_Some_elem_of [lemma, in bedrock.prelude.list]head_list_take [lemma, in bedrock.prelude.list_numbers]
head_list [definition, in bedrock.prelude.list_numbers]
Hnf [abbreviation, in bedrock.prelude.base]
HostInt [constructor, in bedrock.prelude.interrupts]
hw_types [library]
I
IdOfBS [record, in bedrock.prelude.named_binder]iff_forall [lemma, in bedrock.prelude.base]
ignore_ws [definition, in bedrock.prelude.parsec]
IM [module, in bedrock.prelude.avl]
implb [section, in bedrock.prelude.bool]
implb_prop_elim [lemma, in bedrock.prelude.bool]
implb_prop_intro [lemma, in bedrock.prelude.bool]
implb_True [lemma, in bedrock.prelude.bool]
implyP [lemma, in bedrock.prelude.bool]
IMR_omap [abbreviation, in bedrock.prelude.avl]
IMR_delete [abbreviation, in bedrock.prelude.avl]
IMR_singleton [abbreviation, in bedrock.prelude.avl]
IMR_mapfold [abbreviation, in bedrock.prelude.avl]
IMR_merge [abbreviation, in bedrock.prelude.avl]
IMR_map [abbreviation, in bedrock.prelude.avl]
IMR_insert [abbreviation, in bedrock.prelude.avl]
IMR_empty [abbreviation, in bedrock.prelude.avl]
IMR_lookup [abbreviation, in bedrock.prelude.avl]
IM_partial_alter [abbreviation, in bedrock.prelude.avl]
IM_delete [abbreviation, in bedrock.prelude.avl]
IM_singleton [abbreviation, in bedrock.prelude.avl]
IM_mapfold [abbreviation, in bedrock.prelude.avl]
IM_merge [abbreviation, in bedrock.prelude.avl]
IM_map [abbreviation, in bedrock.prelude.avl]
IM_insert [abbreviation, in bedrock.prelude.avl]
IM_empty [abbreviation, in bedrock.prelude.avl]
IM_lookup [abbreviation, in bedrock.prelude.avl]
IM.eqL [lemma, in bedrock.prelude.avl]
inhabited [library]
initialIntConfig [definition, in bedrock.prelude.interrupts]
inj2_inj [instance, in bedrock.prelude.base]
inj2_iff [lemma, in bedrock.prelude.base]
insertN [abbreviation, in bedrock.prelude.list_numbers]
insertN_simpl [definition, in bedrock.prelude.list_numbers]
insertN_takeN_dropN [lemma, in bedrock.prelude.list_numbers]
insertN_explode [lemma, in bedrock.prelude.list_numbers]
insertN_replicateN [lemma, in bedrock.prelude.list_numbers]
insertN_app_r [lemma, in bedrock.prelude.list_numbers]
insertN_app_l [lemma, in bedrock.prelude.list_numbers]
insertN_comm [lemma, in bedrock.prelude.list_numbers]
insertN_insertN [lemma, in bedrock.prelude.list_numbers]
insertN_lengthN [lemma, in bedrock.prelude.list_numbers]
insertN_cons_succ [lemma, in bedrock.prelude.list_numbers]
insertN_cons_zero [lemma, in bedrock.prelude.list_numbers]
insertN_nil [lemma, in bedrock.prelude.list_numbers]
insertN_id [lemma, in bedrock.prelude.list_numbers]
insertN_seqN [lemma, in bedrock.prelude.list_numbers]
insertZ_preserves_sliceZ [lemma, in bedrock.prelude.list_numbers]
insertZ_id [lemma, in bedrock.prelude.list_numbers]
insertZ_simpl [definition, in bedrock.prelude.list_numbers]
insertZ_oob [lemma, in bedrock.prelude.list_numbers]
insertZ_nil [lemma, in bedrock.prelude.list_numbers]
insertZ_app_r [lemma, in bedrock.prelude.list_numbers]
insertZ_app_l [lemma, in bedrock.prelude.list_numbers]
insertZ_app_iff [lemma, in bedrock.prelude.list_numbers]
insertZ_cons_nz [lemma, in bedrock.prelude.list_numbers]
insertZ_cons_z [lemma, in bedrock.prelude.list_numbers]
insertZ_cons_iff [lemma, in bedrock.prelude.list_numbers]
insertZ_eq_insertN [lemma, in bedrock.prelude.list_numbers]
insert_seq [lemma, in bedrock.prelude.list_numbers]
IntAction [record, in bedrock.prelude.interrupts]
IntAction_eq_dec [instance, in bedrock.prelude.interrupts]
IntAction_inhabited [instance, in bedrock.prelude.interrupts]
intcfg_valid_decision [instance, in bedrock.prelude.interrupts]
intcfg_valid [definition, in bedrock.prelude.interrupts]
IntConfig [record, in bedrock.prelude.interrupts]
IntEnabled [constructor, in bedrock.prelude.interrupts]
InteropTests [module, in bedrock.prelude.elpi.derive_test]
InteropTests.A1 [constructor, in bedrock.prelude.elpi.derive_test]
InteropTests.A2 [constructor, in bedrock.prelude.elpi.derive_test]
InteropTests.B1 [constructor, in bedrock.prelude.elpi.derive_test]
InteropTests.B2 [constructor, in bedrock.prelude.elpi.derive_test]
InteropTests.C1 [constructor, in bedrock.prelude.elpi.derive_test]
InteropTests.C2 [constructor, in bedrock.prelude.elpi.derive_test]
InteropTests.manual_T2_finite [instance, in bedrock.prelude.elpi.derive_test]
InteropTests.T1 [inductive, in bedrock.prelude.elpi.derive_test]
InteropTests.T1_finite [definition, in bedrock.prelude.elpi.derive_test]
InteropTests.T1_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
InteropTests.T1_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
InteropTests.T1_eq_dec [instance, in bedrock.prelude.elpi.derive_test]
InteropTests.T2 [inductive, in bedrock.prelude.elpi.derive_test]
InteropTests.T2_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
interrupts [library]
InterruptSignal [inductive, in bedrock.prelude.interrupts]
InterruptSignal_eq_dec [instance, in bedrock.prelude.interrupts]
InterruptSignal_inhabited [instance, in bedrock.prelude.interrupts]
IntLines [record, in bedrock.prelude.interrupts]
IntLines [inductive, in bedrock.prelude.interrupts]
intline_elem_of_dec [instance, in bedrock.prelude.interrupts]
intline_of [projection, in bedrock.prelude.interrupts]
intline_of [constructor, in bedrock.prelude.interrupts]
IntMasked [constructor, in bedrock.prelude.interrupts]
IntOwner [inductive, in bedrock.prelude.interrupts]
into_exist_named_binder [instance, in bedrock.prelude.named_binder]
introT [lemma, in bedrock.prelude.bool]
IntStatus [inductive, in bedrock.prelude.interrupts]
IntTrigger [inductive, in bedrock.prelude.interrupts]
int_line [module, in bedrock.prelude.hw_types]
int_types_match_decision [instance, in bedrock.prelude.interrupts]
int_types_match [definition, in bedrock.prelude.interrupts]
int_trigger_match_dec [instance, in bedrock.prelude.interrupts]
int_trigger_match [definition, in bedrock.prelude.interrupts]
int_cfg_decision [instance, in bedrock.prelude.interrupts]
int_config_inhabited [instance, in bedrock.prelude.interrupts]
INT_config_of [definition, in bedrock.prelude.interrupts]
int_status [projection, in bedrock.prelude.interrupts]
int_owner [projection, in bedrock.prelude.interrupts]
int_trigger [projection, in bedrock.prelude.interrupts]
int_cpu [projection, in bedrock.prelude.interrupts]
int_status_decision [instance, in bedrock.prelude.interrupts]
int_status_inhabited [instance, in bedrock.prelude.interrupts]
int_owner_decision [instance, in bedrock.prelude.interrupts]
int_owner_inhabited [instance, in bedrock.prelude.interrupts]
int_trigger_decision [instance, in bedrock.prelude.interrupts]
int_trigger_inhabited [instance, in bedrock.prelude.interrupts]
iso [module, in bedrock.prelude.lens]
iso.f [projection, in bedrock.prelude.lens]
iso.f_g [projection, in bedrock.prelude.lens]
iso.g [projection, in bedrock.prelude.lens]
iso.g_f [projection, in bedrock.prelude.lens]
iso.inv [definition, in bedrock.prelude.lens]
iso.lawsT [record, in bedrock.prelude.lens]
iso.t [record, in bedrock.prelude.lens]
iso2lens [definition, in bedrock.prelude.lens]
iso2lens_laws [lemma, in bedrock.prelude.lens]
isSome [definition, in bedrock.prelude.option]
isSomeP [lemma, in bedrock.prelude.option]
is_Some_proj_eq [lemma, in bedrock.prelude.option]
Is_true_eq [lemma, in bedrock.prelude.bool]
Is_true_is_true [lemma, in bedrock.prelude.bool]
L
lengthN [definition, in bedrock.prelude.list_numbers]lengthN_sliceZ_le [lemma, in bedrock.prelude.list_numbers]
lengthN_sliceZ [lemma, in bedrock.prelude.list_numbers]
lengthN_rangeZ [lemma, in bedrock.prelude.list_numbers]
lengthN_simplZ [definition, in bedrock.prelude.list_numbers]
lengthN_insertZ [lemma, in bedrock.prelude.list_numbers]
lengthN_zip [lemma, in bedrock.prelude.list_numbers]
lengthN_simpl [definition, in bedrock.prelude.list_numbers]
lengthN_insertN [lemma, in bedrock.prelude.list_numbers]
lengthN_replicateN [lemma, in bedrock.prelude.list_numbers]
lengthN_rotateN [lemma, in bedrock.prelude.list_numbers]
lengthN_takeN [lemma, in bedrock.prelude.list_numbers]
lengthN_dropN [lemma, in bedrock.prelude.list_numbers]
lengthN_map [lemma, in bedrock.prelude.list_numbers]
lengthN_app [lemma, in bedrock.prelude.list_numbers]
lengthN_one [lemma, in bedrock.prelude.list_numbers]
lengthN_cons [lemma, in bedrock.prelude.list_numbers]
lengthN_nil [lemma, in bedrock.prelude.list_numbers]
lengthN_fold [lemma, in bedrock.prelude.list_numbers]
lengthZ [abbreviation, in bedrock.prelude.list_numbers]
lengthZ_sliceZ_iff [lemma, in bedrock.prelude.list_numbers]
lengthZ_eq_sub_iff [lemma, in bedrock.prelude.list_numbers]
length_takeN [lemma, in bedrock.prelude.list_numbers]
length_dropN [lemma, in bedrock.prelude.list_numbers]
length_lengthN [lemma, in bedrock.prelude.list_numbers]
lens [library]
lens [library]
LensLaws' [record, in bedrock.prelude.lens]
lens_assoc [instance, in bedrock.prelude.lens]
lens_right_id [instance, in bedrock.prelude.lens]
lens_left_id [instance, in bedrock.prelude.lens]
lens_union [instance, in bedrock.prelude.lens]
lens_unit [instance, in bedrock.prelude.lens]
lens_aux_1.lens.of_get_put [definition, in bedrock.prelude.lens]
lens_aux_1.lens.of_get_set [definition, in bedrock.prelude.lens]
lens_aux_1.lens [module, in bedrock.prelude.lens]
lens_aux_1 [module, in bedrock.prelude.lens]
Lens_with [definition, in bedrock.prelude.elpi.derive.lens]
letstar [library]
Level [definition, in bedrock.prelude.page]
LevelSig [constructor, in bedrock.prelude.interrupts]
liftM2 [definition, in bedrock.prelude.base]
line [projection, in bedrock.prelude.interrupts]
list [section, in bedrock.prelude.list]
list [library]
listN [section, in bedrock.prelude.list_numbers]
ListNoDup_enum [lemma, in bedrock.prelude.finite]
listN.A [variable, in bedrock.prelude.list_numbers]
lists [section, in bedrock.prelude.list]
listset_nodup_elem_of_dec [instance, in bedrock.prelude.listset_nodup]
listset_nodup [library]
lists.A [variable, in bedrock.prelude.list]
lists.B [variable, in bedrock.prelude.list]
lists.zip_with.C [variable, in bedrock.prelude.list]
lists.zip_with [section, in bedrock.prelude.list]
listZ [section, in bedrock.prelude.list_numbers]
list_ap_compose [lemma, in bedrock.prelude.list]
list_ap_cons_r_p [abbreviation, in bedrock.prelude.list]
list_ap_cons_l [abbreviation, in bedrock.prelude.list]
list_ap_nil_r [abbreviation, in bedrock.prelude.list]
list_ap_nil_l [abbreviation, in bedrock.prelude.list]
list_ap_singleton_r [lemma, in bedrock.prelude.list]
list_ap_singleton_l [lemma, in bedrock.prelude.list]
list_difference_remove [lemma, in bedrock.prelude.list]
list_remove_delete [lemma, in bedrock.prelude.list]
list_difference_delete [lemma, in bedrock.prelude.list]
list_singleton_eq_ext [lemma, in bedrock.prelude.list]
list_empty_eq_ext [lemma, in bedrock.prelude.list]
list_ne_length [lemma, in bedrock.prelude.list]
list_difference_id [abbreviation, in bedrock.prelude.list]
list_difference_singleton_not_in [lemma, in bedrock.prelude.list]
list_difference_app_r [lemma, in bedrock.prelude.list]
list_difference_cons_r [lemma, in bedrock.prelude.list]
list_difference_nil_r [lemma, in bedrock.prelude.list]
list_difference [section, in bedrock.prelude.list]
list_delete_elem_of_2 [lemma, in bedrock.prelude.list]
list_delete_elem_of_1 [lemma, in bedrock.prelude.list]
list_fmap_id' [lemma, in bedrock.prelude.list]
list_fmap_filter [lemma, in bedrock.prelude.list]
list_filter_insert [lemma, in bedrock.prelude.list]
list_filter_empty_iff [lemma, in bedrock.prelude.list]
list_alter_insert [lemma, in bedrock.prelude.list]
list_not_disjoint [lemma, in bedrock.prelude.list]
list_disjoint_dec [instance, in bedrock.prelude.list]
list_disjoint_alt [lemma, in bedrock.prelude.list]
list_bind_perm [instance, in bedrock.prelude.list]
list_bind_mono [instance, in bedrock.prelude.list]
list_equiv_symmetric_strong [lemma, in bedrock.prelude.list]
list_equiv_reflexive_strong [lemma, in bedrock.prelude.list]
list_insertZ [instance, in bedrock.prelude.list_numbers]
list_lookupZ [instance, in bedrock.prelude.list_numbers]
list_alterN_insertN [lemma, in bedrock.prelude.list_numbers]
list_ne_lengthN [lemma, in bedrock.prelude.list_numbers]
list_lookupN_fmap [lemma, in bedrock.prelude.list_numbers]
list_alter_alterN [lemma, in bedrock.prelude.list_numbers]
list_alterN_alter [lemma, in bedrock.prelude.list_numbers]
list_alterN [instance, in bedrock.prelude.list_numbers]
list_insert_insertN [lemma, in bedrock.prelude.list_numbers]
list_insertN_insert [lemma, in bedrock.prelude.list_numbers]
list_insertN [instance, in bedrock.prelude.list_numbers]
list_lookup_lookupN [lemma, in bedrock.prelude.list_numbers]
list_lookupN_lookup [lemma, in bedrock.prelude.list_numbers]
list_lookupN [instance, in bedrock.prelude.list_numbers]
list_to_set_mono [instance, in bedrock.prelude.fin_sets]
list_to_set_elements_cancel_L [instance, in bedrock.prelude.fin_sets]
list_to_set_elements_cancel [instance, in bedrock.prelude.fin_sets]
list_In_enum [lemma, in bedrock.prelude.finite]
list_find_enum_total [lemma, in bedrock.prelude.finite]
list_numbers [library]
list.A [variable, in bedrock.prelude.list]
list.disjoint_dec [section, in bedrock.prelude.list]
lookupN [abbreviation, in bedrock.prelude.list_numbers]
lookupN_seqN [lemma, in bedrock.prelude.list_numbers]
lookupN_seqN_lt [lemma, in bedrock.prelude.list_numbers]
lookupN_seqN_ge [lemma, in bedrock.prelude.list_numbers]
lookupN_ge_None [lemma, in bedrock.prelude.list_numbers]
lookupN_simpl [definition, in bedrock.prelude.list_numbers]
lookupN_explode [lemma, in bedrock.prelude.list_numbers]
lookupN_mid [lemma, in bedrock.prelude.list_numbers]
lookupN_any [lemma, in bedrock.prelude.list_numbers]
lookupN_rotateN [lemma, in bedrock.prelude.list_numbers]
lookupN_map [lemma, in bedrock.prelude.list_numbers]
lookupN_nth_error [lemma, in bedrock.prelude.list_numbers]
lookupN_insertN_neq [lemma, in bedrock.prelude.list_numbers]
lookupN_insertN_eq [lemma, in bedrock.prelude.list_numbers]
lookupN_app_r [lemma, in bedrock.prelude.list_numbers]
lookupN_app_l [lemma, in bedrock.prelude.list_numbers]
lookupN_tail [lemma, in bedrock.prelude.list_numbers]
lookupN_head [lemma, in bedrock.prelude.list_numbers]
lookupN_replicateN [lemma, in bedrock.prelude.list_numbers]
lookupN_bound [lemma, in bedrock.prelude.list_numbers]
lookupN_is_None [lemma, in bedrock.prelude.list_numbers]
lookupN_is_Some [lemma, in bedrock.prelude.list_numbers]
lookupN_takeN [lemma, in bedrock.prelude.list_numbers]
lookupN_dropN [lemma, in bedrock.prelude.list_numbers]
lookupN_cons_succ [lemma, in bedrock.prelude.list_numbers]
lookupN_cons_Nsucc [lemma, in bedrock.prelude.list_numbers]
lookupN_cons_zero [lemma, in bedrock.prelude.list_numbers]
lookupN_nil [lemma, in bedrock.prelude.list_numbers]
lookupN_fold [lemma, in bedrock.prelude.list_numbers]
lookupZ_simpl [definition, in bedrock.prelude.list_numbers]
lookupZ_singleton_Some [lemma, in bedrock.prelude.list_numbers]
lookupZ_insertZ_neq [lemma, in bedrock.prelude.list_numbers]
lookupZ_insertZ_eq [lemma, in bedrock.prelude.list_numbers]
lookupZ_insertZ [lemma, in bedrock.prelude.list_numbers]
lookupZ_cons [lemma, in bedrock.prelude.list_numbers]
lookupZ_app [lemma, in bedrock.prelude.list_numbers]
lookupZ_nil [lemma, in bedrock.prelude.list_numbers]
lookupZ_is_Some [lemma, in bedrock.prelude.list_numbers]
lookupZ_None_inv [lemma, in bedrock.prelude.list_numbers]
lookupZ_None [lemma, in bedrock.prelude.list_numbers]
lookupZ_Some_to_N [lemma, in bedrock.prelude.list_numbers]
lookupZ_Some_to_nat [lemma, in bedrock.prelude.list_numbers]
lookup_insert_iff [lemma, in bedrock.prelude.gmap]
lookup_insert [section, in bedrock.prelude.gmap]
lookup_from_ctorlist [definition, in bedrock.prelude.elpi.derive.countable]
LTS [abbreviation, in bedrock.prelude.sts]
lts_init_state [abbreviation, in bedrock.prelude.sts]
lts_step [abbreviation, in bedrock.prelude.sts]
lts_state [abbreviation, in bedrock.prelude.sts]
Lt_Eq_discr [definition, in bedrock.prelude.numbers]
Lt_Gt_discr [definition, in bedrock.prelude.numbers]
M
M [abbreviation, in bedrock.prelude.parsec]mapM_fmap_Forall_Some_inv [lemma, in bedrock.prelude.list]
map_to_list_elements [abbreviation, in bedrock.prelude.avl]
map_canon [abbreviation, in bedrock.prelude.avl]
map_inj [instance, in bedrock.prelude.list]
map_fmap [lemma, in bedrock.prelude.list]
map_insertN [lemma, in bedrock.prelude.list_numbers]
map_Forall_fmap [lemma, in bedrock.prelude.fin_maps]
map_fmap_difference [lemma, in bedrock.prelude.fin_maps]
map_insert_difference [lemma, in bedrock.prelude.fin_maps]
map_difference_insert_ne [lemma, in bedrock.prelude.fin_maps]
map_difference_union_distr_disj_l [lemma, in bedrock.prelude.fin_maps]
map_difference_union_distr_l [lemma, in bedrock.prelude.fin_maps]
map_union_difference [lemma, in bedrock.prelude.fin_maps]
map_positive_r [lemma, in bedrock.prelude.fin_maps]
map_positive [lemma, in bedrock.prelude.fin_maps]
MkWrapN_inj [instance, in bedrock.prelude.wrap]
mmio_idx [module, in bedrock.prelude.hw_types]
MonadNotations [module, in bedrock.prelude.base]
funM _ .. _ => _ (function_scope) [notation, in bedrock.prelude.base]
let* := _ in _ (monad_scope) [notation, in bedrock.prelude.base]
let* _ , .. , _ := _ in _ (monad_scope) [notation, in bedrock.prelude.base]
(>>=) (stdpp_scope) [notation, in bedrock.prelude.base]
(.>>= _ ) (stdpp_scope) [notation, in bedrock.prelude.base]
( _ >>=.) (stdpp_scope) [notation, in bedrock.prelude.base]
_ >>=@{ _ } _ (stdpp_scope) [notation, in bedrock.prelude.base]
_ ≫= _ (stdpp_scope) [notation, in bedrock.prelude.base]
_ >>= _ (stdpp_scope) [notation, in bedrock.prelude.base]
letM* := _ in _ (stdpp_scope) [notation, in bedrock.prelude.base]
letM* _ , .. , _ := _ in _ (stdpp_scope) [notation, in bedrock.prelude.base]
monad_ap [instance, in bedrock.prelude.base]
monoid [section, in bedrock.prelude.lens]
monoid.A [variable, in bedrock.prelude.lens]
N
name [library]NamedBinder [definition, in bedrock.prelude.named_binder]
named_binder [library]
Names [record, in bedrock.prelude.name]
name_inhabited [projection, in bedrock.prelude.name]
name_finite [projection, in bedrock.prelude.name]
name_eq_dec [projection, in bedrock.prelude.name]
nat_fin_iter_le [lemma, in bedrock.prelude.list_numbers]
nat_fin_iter_lt [lemma, in bedrock.prelude.list_numbers]
Nat_shiftr_right_id [instance, in bedrock.prelude.numbers]
Nat_shiftr_left_absorb [instance, in bedrock.prelude.numbers]
Nat_shiftl_right_id [instance, in bedrock.prelude.numbers]
Nat_shiftl_left_absorb [instance, in bedrock.prelude.numbers]
Nat_lor_right_id [instance, in bedrock.prelude.numbers]
Nat_lor_left_id [instance, in bedrock.prelude.numbers]
Nat_lor_assoc [instance, in bedrock.prelude.numbers]
Nat_lor_comm [instance, in bedrock.prelude.numbers]
Nat_land_right_absorb [instance, in bedrock.prelude.numbers]
Nat_land_left_absorb [instance, in bedrock.prelude.numbers]
Nat_land_assoc [instance, in bedrock.prelude.numbers]
Nat_land_comm [instance, in bedrock.prelude.numbers]
Nat_max_assoc [instance, in bedrock.prelude.numbers]
Nat_max_comm [instance, in bedrock.prelude.numbers]
Nat_min_assoc [instance, in bedrock.prelude.numbers]
Nat_min_comm [instance, in bedrock.prelude.numbers]
Nat_trychotomyT [instance, in bedrock.prelude.numbers]
Nat_mul_right_absorb [instance, in bedrock.prelude.numbers]
Nat_mul_left_absorb [instance, in bedrock.prelude.numbers]
Nat_mul_right_id [instance, in bedrock.prelude.numbers]
Nat_mul_left_id [instance, in bedrock.prelude.numbers]
Nat_mul_comm [instance, in bedrock.prelude.numbers]
Nat_mul_assoc [instance, in bedrock.prelude.numbers]
Nat_add_right_id [instance, in bedrock.prelude.numbers]
Nat_add_left_id [instance, in bedrock.prelude.numbers]
Nat_add_comm [instance, in bedrock.prelude.numbers]
Nat_add_assoc [instance, in bedrock.prelude.numbers]
nat_compare [instance, in bedrock.prelude.numbers]
Nat2N_id_cancel [instance, in bedrock.prelude.numbers]
Nat2Z_id_cancel [instance, in bedrock.prelude.numbers]
negP [lemma, in bedrock.prelude.bool]
NNonZero [record, in bedrock.prelude.base]
NNonZero [inductive, in bedrock.prelude.base]
NoDup_fmap_ap [lemma, in bedrock.prelude.list]
NoDup_fmap_ap.C [variable, in bedrock.prelude.list]
NoDup_fmap_ap.B [variable, in bedrock.prelude.list]
NoDup_fmap_ap.A [variable, in bedrock.prelude.list]
NoDup_fmap_ap [section, in bedrock.prelude.list]
NoDup_ap [lemma, in bedrock.prelude.list]
NoDup_fmap_fun [lemma, in bedrock.prelude.list]
NoDup_ap.C [variable, in bedrock.prelude.list]
NoDup_ap.B [variable, in bedrock.prelude.list]
NoDup_ap.A [variable, in bedrock.prelude.list]
NoDup_ap [section, in bedrock.prelude.list]
NoDup_zip_snd [lemma, in bedrock.prelude.list]
NoDup_zip_fst [lemma, in bedrock.prelude.list]
NoDup_zip_with_snd_inj [lemma, in bedrock.prelude.list]
NoDup_zip_with_snd_gen [lemma, in bedrock.prelude.list]
NoDup_zip_with_fst_inj [lemma, in bedrock.prelude.list]
NoDup_zip_with_fst_gen [lemma, in bedrock.prelude.list]
NoDup_not_in_delete [lemma, in bedrock.prelude.list]
NoDup_Permutation' [lemma, in bedrock.prelude.list]
NoDup_rangeZ [lemma, in bedrock.prelude.list_numbers]
NoDup_seqN [lemma, in bedrock.prelude.list_numbers]
NoDup_app_fmap_l [lemma, in bedrock.prelude.finite]
notations [library]
not_elem_of_list_lookup [lemma, in bedrock.prelude.list]
not_or [lemma, in bedrock.prelude.base]
not_pairwise_disjoint [lemma, in bedrock.prelude.fin_sets]
not_set_elem_of_bool_decide [lemma, in bedrock.prelude.fin_sets]
numbers [library]
N_non_empty [instance, in bedrock.prelude.base]
N_non_zero [projection, in bedrock.prelude.base]
N_non_zero [constructor, in bedrock.prelude.base]
N_enumerate [lemma, in bedrock.prelude.list_numbers]
N_fin_iter_le [lemma, in bedrock.prelude.list_numbers]
N_fin_iter_lt [lemma, in bedrock.prelude.list_numbers]
N_to_Qp_mul [lemma, in bedrock.prelude.numbers]
N_to_Qp_add [lemma, in bedrock.prelude.numbers]
N_to_Qp_inj_lt [lemma, in bedrock.prelude.numbers]
N_to_Qp_inj_le [lemma, in bedrock.prelude.numbers]
N_to_Qp_inj_iff [lemma, in bedrock.prelude.numbers]
N_to_Qp_inj [lemma, in bedrock.prelude.numbers]
N_to_Qp_succ [lemma, in bedrock.prelude.numbers]
N_to_Qp_pos [lemma, in bedrock.prelude.numbers]
N_to_Qp_1 [lemma, in bedrock.prelude.numbers]
N_to_Qp [definition, in bedrock.prelude.numbers]
N_b2n_1 [lemma, in bedrock.prelude.numbers]
N_b2n_0 [lemma, in bedrock.prelude.numbers]
N_b2n_inj [instance, in bedrock.prelude.numbers]
N_mul_divide_weaken_r [lemma, in bedrock.prelude.numbers]
N_mul_divide_weaken_l [lemma, in bedrock.prelude.numbers]
N_divide_add_cancel_l [lemma, in bedrock.prelude.numbers]
N_divide_dec [instance, in bedrock.prelude.numbers]
N_lxor_lt_pow2 [lemma, in bedrock.prelude.numbers]
N_lxor_lt_pow2_aux [lemma, in bedrock.prelude.numbers]
N_le_pred_lt [lemma, in bedrock.prelude.numbers]
N_lxor_mono_aux [lemma, in bedrock.prelude.numbers]
N_lor_mono_r [lemma, in bedrock.prelude.numbers]
N_land_mono_l [lemma, in bedrock.prelude.numbers]
N_land_mono_r [lemma, in bedrock.prelude.numbers]
N_setbit_bool_decide [lemma, in bedrock.prelude.numbers]
N_ones_spec [lemma, in bedrock.prelude.numbers]
N_leb_bool_decide [lemma, in bedrock.prelude.numbers]
N_eqb_bool_decide [lemma, in bedrock.prelude.numbers]
N_succ_lt_mono_inv [lemma, in bedrock.prelude.numbers]
N_of_nat_le_mono [lemma, in bedrock.prelude.numbers]
N_of_nat_lt_mono [lemma, in bedrock.prelude.numbers]
N_succ_pos_pred [lemma, in bedrock.prelude.numbers]
N_land_bit [lemma, in bedrock.prelude.numbers]
N_ext_iff [lemma, in bedrock.prelude.numbers]
N_ext [lemma, in bedrock.prelude.numbers]
N_minE [lemma, in bedrock.prelude.numbers]
N_succ_inj [instance, in bedrock.prelude.numbers]
N_shiftr_right_id [instance, in bedrock.prelude.numbers]
N_shiftr_left_absorb [instance, in bedrock.prelude.numbers]
N_shiftl_right_id [instance, in bedrock.prelude.numbers]
N_shiftl_left_absorb [instance, in bedrock.prelude.numbers]
N_lor_right_id [instance, in bedrock.prelude.numbers]
N_lor_left_id [instance, in bedrock.prelude.numbers]
N_lor_assoc [instance, in bedrock.prelude.numbers]
N_lor_comm [instance, in bedrock.prelude.numbers]
N_land_right_absorb [instance, in bedrock.prelude.numbers]
N_land_left_absorb [instance, in bedrock.prelude.numbers]
N_land_assoc [instance, in bedrock.prelude.numbers]
N_land_comm [instance, in bedrock.prelude.numbers]
N_max_assoc [instance, in bedrock.prelude.numbers]
N_max_comm [instance, in bedrock.prelude.numbers]
N_min_assoc [instance, in bedrock.prelude.numbers]
N_min_comm [instance, in bedrock.prelude.numbers]
N_trychotomyT [instance, in bedrock.prelude.numbers]
N_mul_right_absorb [instance, in bedrock.prelude.numbers]
N_mul_left_absorb [instance, in bedrock.prelude.numbers]
N_mul_right_id [instance, in bedrock.prelude.numbers]
N_mul_left_id [instance, in bedrock.prelude.numbers]
N_mul_comm [instance, in bedrock.prelude.numbers]
N_mul_assoc [instance, in bedrock.prelude.numbers]
N_add_right_id [instance, in bedrock.prelude.numbers]
N_add_left_id [instance, in bedrock.prelude.numbers]
N_add_comm [instance, in bedrock.prelude.numbers]
N_add_assoc [instance, in bedrock.prelude.numbers]
N_comparison [instance, in bedrock.prelude.numbers]
N_compare [instance, in bedrock.prelude.numbers]
N2Nat_inj_le [lemma, in bedrock.prelude.list_numbers]
N2Nat_id_cancel [instance, in bedrock.prelude.numbers]
N2Z_inj_divide [lemma, in bedrock.prelude.numbers]
N2Z_lnot [lemma, in bedrock.prelude.numbers]
N2Z_lnot_trim [lemma, in bedrock.prelude.numbers]
N2Z_lxor [lemma, in bedrock.prelude.numbers]
N2Z_shiftr [lemma, in bedrock.prelude.numbers]
N2Z_shiftl [lemma, in bedrock.prelude.numbers]
N2Z_lor [lemma, in bedrock.prelude.numbers]
N2Z_land [lemma, in bedrock.prelude.numbers]
N2Z_id_cancel [instance, in bedrock.prelude.numbers]
O
on [abbreviation, in bedrock.prelude.option]on_props.on_total_order [instance, in bedrock.prelude.option]
on_props.on_partial_order [instance, in bedrock.prelude.option]
on_props.on_trichotomyT [instance, in bedrock.prelude.option]
on_props.on_trichotomy [instance, in bedrock.prelude.option]
on_props.on_antisymm_eq_inj [instance, in bedrock.prelude.option]
on_props.on_antisymm [instance, in bedrock.prelude.option]
on_props.on_strict_order [instance, in bedrock.prelude.option]
on_props.on_per [instance, in bedrock.prelude.option]
on_props.on_preorder [instance, in bedrock.prelude.option]
on_props.on_equivalence [instance, in bedrock.prelude.option]
on_props.on_transitive [instance, in bedrock.prelude.option]
on_props.on_asymmetric [instance, in bedrock.prelude.option]
on_props.on_symmetric [instance, in bedrock.prelude.option]
on_props.on_irreflexive [instance, in bedrock.prelude.option]
on_props.on_reflexive [instance, in bedrock.prelude.option]
on_props.on_decidable [instance, in bedrock.prelude.option]
on_props.on_props.f [variable, in bedrock.prelude.option]
on_props.on_props.B [variable, in bedrock.prelude.option]
on_props.on_props.A [variable, in bedrock.prelude.option]
on_props.on_props [section, in bedrock.prelude.option]
on_props [module, in bedrock.prelude.option]
opteT [abbreviation, in bedrock.prelude.page]
option [module, in bedrock.prelude.option]
option [library]
option_list_nil [lemma, in bedrock.prelude.option]
option_Forall2_decision [instance, in bedrock.prelude.option]
option.existsb [definition, in bedrock.prelude.option]
option.on [definition, in bedrock.prelude.option]
orb_right_absorb [instance, in bedrock.prelude.bool]
orb_left_absorb [instance, in bedrock.prelude.bool]
orb_right_id [instance, in bedrock.prelude.bool]
orb_left_id [instance, in bedrock.prelude.bool]
orb_assoc' [instance, in bedrock.prelude.bool]
orb_comm' [instance, in bedrock.prelude.bool]
orP [lemma, in bedrock.prelude.bool]
OT_bs.eq_dec [definition, in bedrock.prelude.bytestring_core]
OT_bs.lt_not_eq [lemma, in bedrock.prelude.bytestring_core]
OT_bs.lt_trans [lemma, in bedrock.prelude.bytestring_core]
OT_bs.eq_trans [lemma, in bedrock.prelude.bytestring_core]
OT_bs.eq_sym [lemma, in bedrock.prelude.bytestring_core]
OT_bs.eq_refl [lemma, in bedrock.prelude.bytestring_core]
OT_bs.compare [definition, in bedrock.prelude.bytestring_core]
OT_bs.lm [lemma, in bedrock.prelude.bytestring_core]
OT_bs.lt [definition, in bedrock.prelude.bytestring_core]
OT_bs.eq [definition, in bedrock.prelude.bytestring_core]
OT_bs.t [definition, in bedrock.prelude.bytestring_core]
OT_bs [module, in bedrock.prelude.bytestring_core]
OT_byte.eq_dec [definition, in bedrock.prelude.bytestring_core]
OT_byte.compare [definition, in bedrock.prelude.bytestring_core]
OT_byte.lt_not_eq [lemma, in bedrock.prelude.bytestring_core]
OT_byte.lt_trans [lemma, in bedrock.prelude.bytestring_core]
OT_byte.eq_trans [lemma, in bedrock.prelude.bytestring_core]
OT_byte.eq_sym [lemma, in bedrock.prelude.bytestring_core]
OT_byte.eq_refl [lemma, in bedrock.prelude.bytestring_core]
OT_byte.lt [definition, in bedrock.prelude.bytestring_core]
OT_byte.eq [definition, in bedrock.prelude.bytestring_core]
OT_byte.t [definition, in bedrock.prelude.bytestring_core]
OT_byte [module, in bedrock.prelude.bytestring_core]
over_apply [lemma, in bedrock.prelude.lens]
over_apply_raw [lemma, in bedrock.prelude.lens]
P
paddr [definition, in bedrock.prelude.addr]page [library]
page_offset [definition, in bedrock.prelude.page]
page_align_ofs_eq [lemma, in bedrock.prelude.page]
page_align_dn_offset_of [lemma, in bedrock.prelude.page]
page_offset_of [definition, in bedrock.prelude.page]
page_align_up_below [lemma, in bedrock.prelude.page]
page_align_up_mod [lemma, in bedrock.prelude.page]
page_aligned [abbreviation, in bedrock.prelude.page]
page_align_up [definition, in bedrock.prelude.page]
page_align_dn_mod [lemma, in bedrock.prelude.page]
page_align_dn_below [lemma, in bedrock.prelude.page]
page_align_dn [definition, in bedrock.prelude.page]
PAGE_bits_size [lemma, in bedrock.prelude.page]
PAGE_SIZE [definition, in bedrock.prelude.page]
PAGE_BITS [definition, in bedrock.prelude.page]
PairwiseDisjoint [record, in bedrock.prelude.base]
PairwiseDisjoint [inductive, in bedrock.prelude.base]
pairwise_disj_funs_fmap [lemma, in bedrock.prelude.list]
pairwise_disj_funs_cons [lemma, in bedrock.prelude.list]
pairwise_disj_funs_inj [lemma, in bedrock.prelude.list]
pairwise_disj_funs [definition, in bedrock.prelude.list]
pairwise_disjoint [projection, in bedrock.prelude.base]
pairwise_disjoint [constructor, in bedrock.prelude.base]
pairwise_disjoint_union [lemma, in bedrock.prelude.sets]
pairwise_disjoint_union_2 [lemma, in bedrock.prelude.sets]
pairwise_disjoint_union_1 [lemma, in bedrock.prelude.sets]
pairwise_disjoint_singleton [lemma, in bedrock.prelude.sets]
parsec [library]
pe_name_finite [projection, in bedrock.prelude.name]
pe_name_eq_dec [projection, in bedrock.prelude.name]
Pos [module, in bedrock.prelude.numbers]
positive_comparison [instance, in bedrock.prelude.numbers]
positive_compare [instance, in bedrock.prelude.numbers]
PossiblyEmptyNames [record, in bedrock.prelude.name]
Pos_of_S [lemma, in bedrock.prelude.numbers]
Pos.compare_eq [definition, in bedrock.prelude.numbers]
Pos.compare_cont_eq [definition, in bedrock.prelude.numbers]
Pos.compare_cont_Lt_Eq_discr [abbreviation, in bedrock.prelude.numbers]
Pos.compare_cont_Gt_Eq_discr [abbreviation, in bedrock.prelude.numbers]
Pos.compare_cont_not_Eq_mono [definition, in bedrock.prelude.numbers]
pow2N [definition, in bedrock.prelude.numbers]
pow2N_spec [lemma, in bedrock.prelude.numbers]
pow2N_eq [definition, in bedrock.prelude.numbers]
pow2N_aux [definition, in bedrock.prelude.numbers]
pow2N_def [definition, in bedrock.prelude.numbers]
pred_nat_succ [lemma, in bedrock.prelude.numbers]
prelude [library]
preorder_proper [instance, in bedrock.prelude.base]
proper [library]
propset [library]
propset_singleton_equiv_unit [lemma, in bedrock.prelude.propset]
propset_singleton_equiv [lemma, in bedrock.prelude.propset]
pteT [abbreviation, in bedrock.prelude.page]
Q
Qc_compare [instance, in bedrock.prelude.numbers]Qp [module, in bedrock.prelude.numbers]
qPAGE_SIZE [definition, in bedrock.prelude.page]
Qp_div_right_id [abbreviation, in bedrock.prelude.numbers]
Qp_mul_right_id [abbreviation, in bedrock.prelude.numbers]
Qp_mul_left_id [abbreviation, in bedrock.prelude.numbers]
Qp.add_all [definition, in bedrock.prelude.numbers]
Qp.div_4 [lemma, in bedrock.prelude.numbers]
Qp.div_right_id [instance, in bedrock.prelude.numbers]
Qp.half_half_quarter [lemma, in bedrock.prelude.numbers]
Qp.mul_2_2 [lemma, in bedrock.prelude.numbers]
Qp.mul_div [lemma, in bedrock.prelude.numbers]
Qp.mul_right_id [instance, in bedrock.prelude.numbers]
Qp.mul_left_id [instance, in bedrock.prelude.numbers]
Qp.Qp_all.C [variable, in bedrock.prelude.numbers]
Qp.Qp_all [section, in bedrock.prelude.numbers]
Qp.quarter_half [lemma, in bedrock.prelude.numbers]
Qp.sub_all_Some [lemma, in bedrock.prelude.numbers]
Qp.sub_all_add_all [lemma, in bedrock.prelude.numbers]
Qp.sub_all [definition, in bedrock.prelude.numbers]
Qp.third_two_thirds [lemma, in bedrock.prelude.numbers]
Qp.two_thirds_third [lemma, in bedrock.prelude.numbers]
quoted [definition, in bedrock.prelude.parsec]
Q_compare [instance, in bedrock.prelude.numbers]
R
rangeZ [definition, in bedrock.prelude.list_numbers]rangeZ [section, in bedrock.prelude.list_numbers]
rangeZ_snoc [lemma, in bedrock.prelude.list_numbers]
rangeZ_app [lemma, in bedrock.prelude.list_numbers]
rangeZ_cons [lemma, in bedrock.prelude.list_numbers]
rangeZ_nil [lemma, in bedrock.prelude.list_numbers]
rangeZ_oob [lemma, in bedrock.prelude.list_numbers]
rangeZ' [definition, in bedrock.prelude.list_numbers]
reachable [inductive, in bedrock.prelude.sts]
ReachableDone [constructor, in bedrock.prelude.sts]
ReachableStep [constructor, in bedrock.prelude.sts]
reachable_singleton [lemma, in bedrock.prelude.sts]
reachable_nil [lemma, in bedrock.prelude.sts]
reachable_sind [definition, in bedrock.prelude.sts]
reachable_ind [definition, in bedrock.prelude.sts]
Reduce [abbreviation, in bedrock.prelude.base]
Refine [abbreviation, in bedrock.prelude.base]
reflectPQ [inductive, in bedrock.prelude.bool]
reflexive_proper [instance, in bedrock.prelude.base]
refl_True [lemma, in bedrock.prelude.base]
relations [library]
repeatN [abbreviation, in bedrock.prelude.list_numbers]
repeatN_replicateN [lemma, in bedrock.prelude.list_numbers]
repeat_replicate [lemma, in bedrock.prelude.list]
repeat_replicateN [lemma, in bedrock.prelude.list_numbers]
replicateN [definition, in bedrock.prelude.list_numbers]
replicateN_cons [lemma, in bedrock.prelude.list_numbers]
replicateN_simpl [definition, in bedrock.prelude.list_numbers]
replicateN_succ' [lemma, in bedrock.prelude.list_numbers]
replicateN_succ [lemma, in bedrock.prelude.list_numbers]
replicateN_zero [lemma, in bedrock.prelude.list_numbers]
replicateN_plus [lemma, in bedrock.prelude.list_numbers]
replicateN_S [lemma, in bedrock.prelude.list_numbers]
replicateN_0 [lemma, in bedrock.prelude.list_numbers]
replicateZ [abbreviation, in bedrock.prelude.list_numbers]
reserved_notation [library]
resizeN [definition, in bedrock.prelude.list_numbers]
resizeN_takeN_le [lemma, in bedrock.prelude.list_numbers]
resizeN_le [lemma, in bedrock.prelude.list_numbers]
resizeN_takeN_eq [lemma, in bedrock.prelude.list_numbers]
resizeN_plusN [lemma, in bedrock.prelude.list_numbers]
resizeN_idemp [lemma, in bedrock.prelude.list_numbers]
resizeN_replicateN [lemma, in bedrock.prelude.list_numbers]
resizeN_nil [lemma, in bedrock.prelude.list_numbers]
resizeN_lengthN [lemma, in bedrock.prelude.list_numbers]
resizeN_0 [lemma, in bedrock.prelude.list_numbers]
resizeN_all [lemma, in bedrock.prelude.list_numbers]
resizeN_spec [lemma, in bedrock.prelude.list_numbers]
Rleq_Some [constructor, in bedrock.prelude.option]
Rleq_None [constructor, in bedrock.prelude.option]
Roption_leq_eq_equiv [lemma, in bedrock.prelude.option]
Roption_leq_equiv [lemma, in bedrock.prelude.option]
Roption_leq_inv_l_Some [lemma, in bedrock.prelude.option]
Roption_leq_inv_l_Some_eq [lemma, in bedrock.prelude.option]
Roption_leq_None_inv [lemma, in bedrock.prelude.option]
Roption_leq_Some_l_inv [lemma, in bedrock.prelude.option]
Roption_leq_option_relation [lemma, in bedrock.prelude.option]
Roption_leq.A [variable, in bedrock.prelude.option]
Roption_leq [section, in bedrock.prelude.option]
Roption_leq [inductive, in bedrock.prelude.option]
rotateN [definition, in bedrock.prelude.list_numbers]
rotateN_simpl [definition, in bedrock.prelude.list_numbers]
rotateN_replicateN [lemma, in bedrock.prelude.list_numbers]
rotateN_mid [lemma, in bedrock.prelude.list_numbers]
rotateN_index [lemma, in bedrock.prelude.list_numbers]
rotateN_succ [lemma, in bedrock.prelude.list_numbers]
rotateN_plus [lemma, in bedrock.prelude.list_numbers]
rotateN_modulo' [lemma, in bedrock.prelude.list_numbers]
rotateN_modulo [lemma, in bedrock.prelude.list_numbers]
rotateN_lengthN [lemma, in bedrock.prelude.list_numbers]
rotateN_one [lemma, in bedrock.prelude.list_numbers]
rotateN_zero [lemma, in bedrock.prelude.list_numbers]
rotateN_singleton [lemma, in bedrock.prelude.list_numbers]
rotateN_nil [lemma, in bedrock.prelude.list_numbers]
rotateN_iter [lemma, in bedrock.prelude.list_numbers]
rotateN_fold [lemma, in bedrock.prelude.list_numbers]
round_up_align_up [lemma, in bedrock.prelude.numbers]
round_down_align_dn [lemma, in bedrock.prelude.numbers]
round_up [definition, in bedrock.prelude.numbers]
round_down [definition, in bedrock.prelude.numbers]
rPQ_false [constructor, in bedrock.prelude.bool]
rPQ_true [constructor, in bedrock.prelude.bool]
run_full_bs [definition, in bedrock.prelude.parsec]
run_bs [definition, in bedrock.prelude.parsec]
rwP [lemma, in bedrock.prelude.bool]
S
same_property_partial_reflexive [lemma, in bedrock.prelude.option]same_property_reflexive_equiv [lemma, in bedrock.prelude.option]
same_property_intro [lemma, in bedrock.prelude.option]
same_property_iff [lemma, in bedrock.prelude.option]
same_property_per [instance, in bedrock.prelude.option]
same_property.with_on_props [section, in bedrock.prelude.option]
same_property_decision [instance, in bedrock.prelude.option]
same_property.obs [variable, in bedrock.prelude.option]
same_property [section, in bedrock.prelude.option]
same_property [definition, in bedrock.prelude.option]
sc_reflexive [instance, in bedrock.prelude.relations]
semi_set [section, in bedrock.prelude.sets]
semi_set [section, in bedrock.prelude.sets]
sepBy [abbreviation, in bedrock.prelude.bytestring]
seqN [section, in bedrock.prelude.list_numbers]
seqN [definition, in bedrock.prelude.list_numbers]
seqN_sublist [lemma, in bedrock.prelude.list_numbers]
seqN_lengthN [lemma, in bedrock.prelude.list_numbers]
seqN_S_end_app' [lemma, in bedrock.prelude.list_numbers]
seqN_S_end_app [lemma, in bedrock.prelude.list_numbers]
seqN_S_start' [lemma, in bedrock.prelude.list_numbers]
seqN_S_start [lemma, in bedrock.prelude.list_numbers]
seqN_0 [lemma, in bedrock.prelude.list_numbers]
seqW [definition, in bedrock.prelude.wrap]
seqW [section, in bedrock.prelude.wrap]
seqW_S_end_app' [lemma, in bedrock.prelude.wrap]
seqW_S_end_app [lemma, in bedrock.prelude.wrap]
seqW.Phant [variable, in bedrock.prelude.wrap]
sets [library]
set_set [projection, in bedrock.prelude.lens]
set_view [projection, in bedrock.prelude.lens]
set_unfold_list_fmap_ap [instance, in bedrock.prelude.list]
set_unfold_list_ap [instance, in bedrock.prelude.list]
set_unfold_list_omap [instance, in bedrock.prelude.list]
set_unfold_list_mjoin [instance, in bedrock.prelude.list]
set_unfold_list_ret [instance, in bedrock.prelude.list]
set_unfold_in [instance, in bedrock.prelude.list]
set_unfold_list_intersection_with [instance, in bedrock.prelude.list]
set_unfold_list_union [instance, in bedrock.prelude.list]
set_unfold_list_intersection [instance, in bedrock.prelude.list]
set_unfold_list_difference [instance, in bedrock.prelude.list]
set_unfold_list_filter [instance, in bedrock.prelude.list]
set_unfold_list_bind [instance, in bedrock.prelude.list]
set_unfold_elem_of_seqN [instance, in bedrock.prelude.list_numbers]
set_unfold_elem_of_seq [instance, in bedrock.prelude.list_numbers]
set_rangeZ.dom_rangeZ [section, in bedrock.prelude.fin_sets]
set_rangeZ [definition, in bedrock.prelude.fin_sets]
set_rangeZ [section, in bedrock.prelude.fin_sets]
set_concat_map_params [instance, in bedrock.prelude.fin_sets]
set_concat_map_singleton_L [lemma, in bedrock.prelude.fin_sets]
set_concat_map_union_L [lemma, in bedrock.prelude.fin_sets]
set_concat_map_empty_L [lemma, in bedrock.prelude.fin_sets]
set_concat_map.set_concat_map_leibniz [section, in bedrock.prelude.fin_sets]
set_concat_map_singleton [lemma, in bedrock.prelude.fin_sets]
set_concat_map_union [lemma, in bedrock.prelude.fin_sets]
set_unfold_set_concat_map [instance, in bedrock.prelude.fin_sets]
set_concat_map_mono [instance, in bedrock.prelude.fin_sets]
set_concat_map_perm_proper [instance, in bedrock.prelude.fin_sets]
set_concat_map_empty [lemma, in bedrock.prelude.fin_sets]
set_concat_map [definition, in bedrock.prelude.fin_sets]
set_concat_map [section, in bedrock.prelude.fin_sets]
set_map_empty_iff_L [lemma, in bedrock.prelude.fin_sets]
set_map_empty_iff [lemma, in bedrock.prelude.fin_sets]
set_map [abbreviation, in bedrock.prelude.fin_sets]
set_map [section, in bedrock.prelude.fin_sets]
set_map_cancel [instance, in bedrock.prelude.fin_sets]
set_map_ext [lemma, in bedrock.prelude.fin_sets]
set_map_disjoint_singleton_r [lemma, in bedrock.prelude.fin_sets]
set_map_disjoint_singleton_l [lemma, in bedrock.prelude.fin_sets]
set_map_disjoint [lemma, in bedrock.prelude.fin_sets]
set_map_inj_L [instance, in bedrock.prelude.fin_sets]
set_map_inj [instance, in bedrock.prelude.fin_sets]
set_map [abbreviation, in bedrock.prelude.fin_sets]
set_map [section, in bedrock.prelude.fin_sets]
set_map_compose_L [lemma, in bedrock.prelude.fin_sets]
set_map_compose [lemma, in bedrock.prelude.fin_sets]
set_map_functorial.compose.g [variable, in bedrock.prelude.fin_sets]
set_map_functorial.compose.f [variable, in bedrock.prelude.fin_sets]
set_map_functorial.compose [section, in bedrock.prelude.fin_sets]
set_map_id_L [lemma, in bedrock.prelude.fin_sets]
set_map_id [lemma, in bedrock.prelude.fin_sets]
set_map_functorial [section, in bedrock.prelude.fin_sets]
set_seq [section, in bedrock.prelude.fin_sets]
set_elem_of_bool_decide [lemma, in bedrock.prelude.fin_sets]
set_not_disjoint [lemma, in bedrock.prelude.fin_sets]
set_not_Forall [lemma, in bedrock.prelude.fin_sets]
set_not_elem_of [lemma, in bedrock.prelude.fin_sets]
set_unfold_gset_bind [instance, in bedrock.prelude.gmap]
set_Forall_union_equiv [lemma, in bedrock.prelude.sets]
set_disjoint_not_Forall_2 [lemma, in bedrock.prelude.sets]
set_disjoint_not_Forall_1 [lemma, in bedrock.prelude.sets]
set_pairwise_disjoint_symmetric [instance, in bedrock.prelude.sets]
set_pairwise_disjoint [instance, in bedrock.prelude.sets]
set_unfold_bool_decide [instance, in bedrock.prelude.bool]
set_unfold_orb [instance, in bedrock.prelude.bool]
set_unfold_andb [instance, in bedrock.prelude.bool]
set_unfold_negb [instance, in bedrock.prelude.bool]
set_unfold_decode_N_None [instance, in bedrock.prelude.finite]
set_unfold_decode_N_Some [instance, in bedrock.prelude.finite]
set_unfold_finite_preimage_set [instance, in bedrock.prelude.finite]
set_unfold_finite_inverse_inj_Some [instance, in bedrock.prelude.finite]
set_unfold_finite_inverse_None [instance, in bedrock.prelude.finite]
set_unfold_finite_preimage [instance, in bedrock.prelude.finite]
set_unfold_elem_of_enum [instance, in bedrock.prelude.finite]
SimpleBitsetTest [module, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.A [constructor, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.B [constructor, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.C [constructor, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.D [constructor, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature [module, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature [inductive, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature_set [module, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature_finite [definition, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature.t [definition, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature.t_finite [definition, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature.t_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.Unnamed_thm1 [definition, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.Unnamed_thm0 [definition, in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.Unnamed_thm [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest [module, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.A [constructor, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.A [constructor, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.B [constructor, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.B [constructor, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.C [constructor, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.C [constructor, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.D [constructor, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.D [constructor, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature [module, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature [inductive, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature [module, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature [inductive, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite_subproof_elem_of [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite_subproof_nodup [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t_finite [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t_finite [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t_eq_dec [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.Unnamed_thm0 [definition, in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.Unnamed_thm [definition, in bedrock.prelude.elpi.derive_test]
simple_finite_bits [module, in bedrock.prelude.finite]
simple_finite_bits_aux.land_mask_idemp [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.mask_top_land_to_bits [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.all_bits_mask_top [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.N_testbit_mask_top_of_bit [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.to_bits_mod_pow2 [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.N_testbit_to_bits_high_false [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.N_testbit_to_bits' [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.N_testbit_all_bits [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.masked_opt_max [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.masked_max [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux.of_bits_max [lemma, in bedrock.prelude.finite]
simple_finite_bits_aux [module, in bedrock.prelude.finite]
simple_finite_bitmask_type_intf [module, in bedrock.prelude.finite]
simple_finite_bitmask_type_mixin.to_list_max [lemma, in bedrock.prelude.finite]
simple_finite_bitmask_type_mixin.all_bits [definition, in bedrock.prelude.finite]
simple_finite_bitmask_type_mixin [module, in bedrock.prelude.finite]
size_bytes [module, in bedrock.prelude.hw_types]
size_set_rangeZ [lemma, in bedrock.prelude.fin_sets]
size_map_inj [lemma, in bedrock.prelude.fin_sets]
size_set_seq [lemma, in bedrock.prelude.fin_sets]
size_empty_iff_L [lemma, in bedrock.prelude.fin_sets]
sliceZ [definition, in bedrock.prelude.list_numbers]
sliceZ [section, in bedrock.prelude.list_numbers]
sliceZ_insertN [lemma, in bedrock.prelude.list_numbers]
sliceZ_min_l [lemma, in bedrock.prelude.list_numbers]
sliceZ_max_r [lemma, in bedrock.prelude.list_numbers]
sliceZ_explode_insert [lemma, in bedrock.prelude.list_numbers]
sliceZ_explode [lemma, in bedrock.prelude.list_numbers]
sliceZ_app [lemma, in bedrock.prelude.list_numbers]
sliceZ_snoc_insertZ [lemma, in bedrock.prelude.list_numbers]
sliceZ_cons_insertZ [lemma, in bedrock.prelude.list_numbers]
sliceZ_snoc [lemma, in bedrock.prelude.list_numbers]
sliceZ_cons [lemma, in bedrock.prelude.list_numbers]
sliceZ_nil [lemma, in bedrock.prelude.list_numbers]
sliceZ_self [lemma, in bedrock.prelude.list_numbers]
sliceZ_crop [lemma, in bedrock.prelude.list_numbers]
sliceZ_crop_r [lemma, in bedrock.prelude.list_numbers]
sliceZ_crop_l [lemma, in bedrock.prelude.list_numbers]
some_Forall2_eq_iff [lemma, in bedrock.prelude.option]
some_Forall2_eq.A [variable, in bedrock.prelude.option]
some_Forall2_eq [section, in bedrock.prelude.option]
some_Forall2_decision [instance, in bedrock.prelude.option]
some_Forall2_iff [lemma, in bedrock.prelude.option]
some_Forall2_per [instance, in bedrock.prelude.option]
some_Forall2_transitive [instance, in bedrock.prelude.option]
some_Forall2_symmetric [instance, in bedrock.prelude.option]
some_Forall2.R [variable, in bedrock.prelude.option]
some_Forall2 [section, in bedrock.prelude.option]
some_Forall2_unlock_subterm [definition, in bedrock.prelude.option]
some_Forall2.unlock [definition, in bedrock.prelude.option]
some_Forall2.body [definition, in bedrock.prelude.option]
some_Forall2 [module, in bedrock.prelude.option]
some_Forall2_Locked.unlock [axiom, in bedrock.prelude.option]
some_Forall2_Locked.body [axiom, in bedrock.prelude.option]
some_Forall2_Locked [module, in bedrock.prelude.option]
stdpp_ssreflect [library]
Sts [module, in bedrock.prelude.sts]
sts [library]
Sts.hide [definition, in bedrock.prelude.sts]
Sts.HIDE [constructor, in bedrock.prelude.sts]
Sts.hide [section, in bedrock.prelude.sts]
Sts.Hide_step [inductive, in bedrock.prelude.sts]
Sts.hide.L [variable, in bedrock.prelude.sts]
Sts.hide.P [variable, in bedrock.prelude.sts]
Sts.init_state [definition, in bedrock.prelude.sts]
Sts.Label [projection, in bedrock.prelude.sts]
Sts.map [definition, in bedrock.prelude.sts]
Sts.map [section, in bedrock.prelude.sts]
Sts.MAP_action [constructor, in bedrock.prelude.sts]
Sts.MAP_tau [constructor, in bedrock.prelude.sts]
Sts.Map_step [inductive, in bedrock.prelude.sts]
Sts.map.f [variable, in bedrock.prelude.sts]
Sts.map.L [variable, in bedrock.prelude.sts]
Sts.map.L' [variable, in bedrock.prelude.sts]
Sts.map.STS [variable, in bedrock.prelude.sts]
Sts.par [definition, in bedrock.prelude.sts]
Sts.par [section, in bedrock.prelude.sts]
Sts.PAR_right [constructor, in bedrock.prelude.sts]
Sts.PAR_left [constructor, in bedrock.prelude.sts]
Sts.PAR_comm [constructor, in bedrock.prelude.sts]
Sts.Par_step [inductive, in bedrock.prelude.sts]
Sts.par.dual [variable, in bedrock.prelude.sts]
Sts.par.e [variable, in bedrock.prelude.sts]
Sts.par.L [variable, in bedrock.prelude.sts]
Sts.par.R [variable, in bedrock.prelude.sts]
Sts.State [definition, in bedrock.prelude.sts]
Sts.step [definition, in bedrock.prelude.sts]
Sts.step_star_ext [definition, in bedrock.prelude.sts]
Sts.step_star_tau_comp [lemma, in bedrock.prelude.sts]
Sts.step_star_comp [lemma, in bedrock.prelude.sts]
Sts.step_star_tau [definition, in bedrock.prelude.sts]
Sts.step_star [definition, in bedrock.prelude.sts]
Sts.sts [record, in bedrock.prelude.sts]
Sts.t [record, in bedrock.prelude.sts]
Sts._sts [projection, in bedrock.prelude.sts]
Sts._step [projection, in bedrock.prelude.sts]
Sts._init_state [projection, in bedrock.prelude.sts]
Sts._state [projection, in bedrock.prelude.sts]
subrelation_flip [lemma, in bedrock.prelude.base]
subset_of_enum [lemma, in bedrock.prelude.finite]
succ_wrapper.seqW [abbreviation, in bedrock.prelude.wrap]
succ_wrapper.succ [abbreviation, in bedrock.prelude.wrap]
succ_wrapper [module, in bedrock.prelude.wrap]
sum [module, in bedrock.prelude.sum]
sum [library]
sum.existsb [definition, in bedrock.prelude.sum]
T
tail_length_eq [lemma, in bedrock.prelude.list]tail_length [lemma, in bedrock.prelude.list]
tail_drop [lemma, in bedrock.prelude.list_numbers]
takeN [definition, in bedrock.prelude.list_numbers]
takeN_sliceZ [lemma, in bedrock.prelude.list_numbers]
takeN_congr [lemma, in bedrock.prelude.list_numbers]
takeN_insertN_lt [lemma, in bedrock.prelude.list_numbers]
takeN_insertN_ge [lemma, in bedrock.prelude.list_numbers]
takeN_resizeN_le [lemma, in bedrock.prelude.list_numbers]
takeN_resizeN_plus [lemma, in bedrock.prelude.list_numbers]
takeN_resizeN [lemma, in bedrock.prelude.list_numbers]
takeN_resizeN_eq [lemma, in bedrock.prelude.list_numbers]
takeN_dropN_commute [lemma, in bedrock.prelude.list_numbers]
takeN_dropN [lemma, in bedrock.prelude.list_numbers]
takeN_takeN [lemma, in bedrock.prelude.list_numbers]
takeN_S_r [lemma, in bedrock.prelude.list_numbers]
takeN_S_r' [lemma, in bedrock.prelude.list_numbers]
takeN_cons_succ [lemma, in bedrock.prelude.list_numbers]
takeN_nil [lemma, in bedrock.prelude.list_numbers]
takeN_app [lemma, in bedrock.prelude.list_numbers]
takeN_singleton [lemma, in bedrock.prelude.list_numbers]
takeN_lengthN [lemma, in bedrock.prelude.list_numbers]
takeN_one [lemma, in bedrock.prelude.list_numbers]
takeN_zero [lemma, in bedrock.prelude.list_numbers]
takeN_replicateN_plus [lemma, in bedrock.prelude.list_numbers]
takeN_replicateN [lemma, in bedrock.prelude.list_numbers]
TCAndT [inductive, in bedrock.prelude.tc_cond_type]
TCAndT_sind [definition, in bedrock.prelude.tc_cond_type]
TCAndT_rec [definition, in bedrock.prelude.tc_cond_type]
TCAndT_ind [definition, in bedrock.prelude.tc_cond_type]
TCAndT_rect [definition, in bedrock.prelude.tc_cond_type]
TCAndT_intro [constructor, in bedrock.prelude.tc_cond_type]
TCElemOf_iff [lemma, in bedrock.prelude.base]
TCForceEq [inductive, in bedrock.prelude.named_binder]
TCForceEq_sind [definition, in bedrock.prelude.named_binder]
TCForceEq_rec [definition, in bedrock.prelude.named_binder]
TCForceEq_ind [definition, in bedrock.prelude.named_binder]
TCForceEq_rect [definition, in bedrock.prelude.named_binder]
TCForceEq_refl [constructor, in bedrock.prelude.named_binder]
TCLeq [inductive, in bedrock.prelude.base]
TCLeq_nat [lemma, in bedrock.prelude.base]
TCLeq_N [lemma, in bedrock.prelude.base]
TCLeq_Z [lemma, in bedrock.prelude.base]
TCLeq_positive [lemma, in bedrock.prelude.base]
TCLeq_iff [lemma, in bedrock.prelude.base]
TCLeq_lt [constructor, in bedrock.prelude.base]
TCLeq_eq [constructor, in bedrock.prelude.base]
TCLt [inductive, in bedrock.prelude.base]
TCLt_nat [lemma, in bedrock.prelude.base]
TCLt_N [lemma, in bedrock.prelude.base]
TCLt_Z [lemma, in bedrock.prelude.base]
TCLt_positive [lemma, in bedrock.prelude.base]
TCLt_iff [lemma, in bedrock.prelude.base]
TCLt_lt [constructor, in bedrock.prelude.base]
TCOrT [inductive, in bedrock.prelude.tc_cond_type]
TCOrT_sind [definition, in bedrock.prelude.tc_cond_type]
TCOrT_rec [definition, in bedrock.prelude.tc_cond_type]
TCOrT_ind [definition, in bedrock.prelude.tc_cond_type]
TCOrT_rect [definition, in bedrock.prelude.tc_cond_type]
TCOrT_r [constructor, in bedrock.prelude.tc_cond_type]
TCOrT_l [constructor, in bedrock.prelude.tc_cond_type]
tc_symmetric [instance, in bedrock.prelude.relations]
tc_reflexive [instance, in bedrock.prelude.relations]
tc_cond_type [library]
telescopes [library]
telescopes [library]
tele_arg_append [definition, in bedrock.prelude.telescopes]
tele_bind_append [definition, in bedrock.prelude.telescopes]
tele_arg_snoc [definition, in bedrock.prelude.telescopes]
tele_bind_snoc [definition, in bedrock.prelude.telescopes]
tele_snoc [definition, in bedrock.prelude.telescopes]
tele_fun_pointwise [definition, in bedrock.prelude.telescopes]
tele_append [definition, in bedrock.prelude.telescopes]
TEST [module, in bedrock.prelude.list]
Test [module, in bedrock.prelude.named_binder]
Test [module, in bedrock.prelude.fin]
TEST.list_ap_interchange [lemma, in bedrock.prelude.list]
TEST.list_ap_morphism [lemma, in bedrock.prelude.list]
TEST.list_ap_compose [lemma, in bedrock.prelude.list]
TEST.list_ap_id [lemma, in bedrock.prelude.list]
Test.test1 [lemma, in bedrock.prelude.fin]
Test.test2 [lemma, in bedrock.prelude.fin]
Test.Unnamed_thm [definition, in bedrock.prelude.named_binder]
Test.Unnamed_thm [definition, in bedrock.prelude.named_binder]
time [module, in bedrock.prelude.hw_types]
to [projection, in bedrock.prelude.interrupts]
ToBit [record, in bedrock.prelude.elpi.derive.bitset]
ToN [record, in bedrock.prelude.elpi.derive.finite_type]
top_set_intersection_top_r_L [instance, in bedrock.prelude.sets]
top_set_intersection_top_l_L [instance, in bedrock.prelude.sets]
top_set.leibniz [section, in bedrock.prelude.sets]
top_set_intersection_top_r [instance, in bedrock.prelude.sets]
top_set_intersection_top_l [instance, in bedrock.prelude.sets]
top_set [section, in bedrock.prelude.sets]
to_nat_lengthN [lemma, in bedrock.prelude.list_numbers]
TO_UPSTREAM_TRANSPARENT.countable_dsig [instance, in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.dsig_eq_dec [instance, in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.dsig_eq_pi [lemma, in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.dsig_transparent.P [variable, in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.dsig_transparent.A [variable, in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.dsig_transparent [section, in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.f_equal_help [lemma, in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.bool_decide_pack [lemma, in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT [module, in bedrock.prelude.fin]
transitive_proper [instance, in bedrock.prelude.base]
TriggerEdge [constructor, in bedrock.prelude.interrupts]
TriggerLevel [constructor, in bedrock.prelude.interrupts]
type [section, in bedrock.prelude.wrap]
types [module, in bedrock.prelude.hw_types]
types.Build_size_bytes [abbreviation, in bedrock.prelude.hw_types]
types.Build_mmio_idx [abbreviation, in bedrock.prelude.hw_types]
types.Build_cpu [abbreviation, in bedrock.prelude.hw_types]
types.Build_time [abbreviation, in bedrock.prelude.hw_types]
types.Build_int_line [abbreviation, in bedrock.prelude.hw_types]
types.cpu [abbreviation, in bedrock.prelude.hw_types]
types.get_size_bytes [abbreviation, in bedrock.prelude.hw_types]
types.get_mmio_idx [abbreviation, in bedrock.prelude.hw_types]
types.get_cpu [abbreviation, in bedrock.prelude.hw_types]
types.get_time [abbreviation, in bedrock.prelude.hw_types]
types.get_int_line [abbreviation, in bedrock.prelude.hw_types]
types.int_line [abbreviation, in bedrock.prelude.hw_types]
types.mmio_idx [abbreviation, in bedrock.prelude.hw_types]
types.size_bytes [abbreviation, in bedrock.prelude.hw_types]
types.time [abbreviation, in bedrock.prelude.hw_types]
U
under_proper [instance, in bedrock.prelude.under_rel_proper]under_flip_mono [instance, in bedrock.prelude.under_rel_proper]
under_mono [instance, in bedrock.prelude.under_rel_proper]
under_proper.R [variable, in bedrock.prelude.under_rel_proper]
under_proper.T [variable, in bedrock.prelude.under_rel_proper]
under_proper [section, in bedrock.prelude.under_rel_proper]
under_rel_proper [library]
Unfold [abbreviation, in bedrock.prelude.base]
union_minus_r_L [lemma, in bedrock.prelude.sets]
union_minus_r [lemma, in bedrock.prelude.sets]
union_minus_l_L [lemma, in bedrock.prelude.sets]
union_minus_l [lemma, in bedrock.prelude.sets]
unwrapN [projection, in bedrock.prelude.wrap]
unwrapN_succ_inj [lemma, in bedrock.prelude.wrap]
unwrapN_inj [instance, in bedrock.prelude.wrap]
V
vaddr [definition, in bedrock.prelude.addr]view_set [projection, in bedrock.prelude.lens]
view_over [projection, in bedrock.prelude.lens]
view_apply [lemma, in bedrock.prelude.lens]
W
_ <= _ (Qp_scope) [notation, in bedrock.prelude.numbers]with_N_to_Qp [section, in bedrock.prelude.numbers]
with_Z [section, in bedrock.prelude.numbers]
wrap [library]
WrapN [record, in bedrock.prelude.wrap]
wrapN_succ [definition, in bedrock.prelude.wrap]
wrapN_add_0w_r [lemma, in bedrock.prelude.wrap]
wrapN_add_0N_r [lemma, in bedrock.prelude.wrap]
wrapN_add_0w_l [lemma, in bedrock.prelude.wrap]
wrapN_add_0N_l [lemma, in bedrock.prelude.wrap]
_ + _ (wrapN_scope) [notation, in bedrock.prelude.wrap]
0 (wrapN_scope) [notation, in bedrock.prelude.wrap]
wrapN_notations.wrapNwrapN_add [instance, in bedrock.prelude.wrap]
wrapN_notations.NwrapN_add [instance, in bedrock.prelude.wrap]
wrapN_notations.wrapNN_add [instance, in bedrock.prelude.wrap]
wrapN_notations.wrapN_add [projection, in bedrock.prelude.wrap]
wrapN_notations.WrapNAdd [record, in bedrock.prelude.wrap]
wrapN_notations.wrapN_add [constructor, in bedrock.prelude.wrap]
wrapN_notations.WrapNAdd [inductive, in bedrock.prelude.wrap]
wrapN_notations [module, in bedrock.prelude.wrap]
wrapN_inhabited [instance, in bedrock.prelude.wrap]
wrapN_countable [instance, in bedrock.prelude.wrap]
wrapN_eq_decision [instance, in bedrock.prelude.wrap]
wrapper [module, in bedrock.prelude.wrap]
wrapper.of_to_N [lemma, in bedrock.prelude.wrap]
wrapper.of_N [definition, in bedrock.prelude.wrap]
wrapper.Phant [inductive, in bedrock.prelude.wrap]
wrapper.t [definition, in bedrock.prelude.wrap]
wrapper.to_of_N [lemma, in bedrock.prelude.wrap]
wrapper.to_N [definition, in bedrock.prelude.wrap]
ws [definition, in bedrock.prelude.parsec]
Z
Zabs2Nat_id_cancel [instance, in bedrock.prelude.numbers]Zabs2N_id_cancel [instance, in bedrock.prelude.numbers]
Zarith_simpl [definition, in bedrock.prelude.list_numbers]
zip_lookup_Some [lemma, in bedrock.prelude.list]
zip_lookupN_Some [lemma, in bedrock.prelude.list_numbers]
Z_rem_dev_eq [lemma, in bedrock.prelude.numbers]
Z_ones_nonneg [lemma, in bedrock.prelude.numbers]
Z_ones_pow2 [lemma, in bedrock.prelude.numbers]
Z_divide_dec [instance, in bedrock.prelude.numbers]
Z_divide_gcd_iff' [lemma, in bedrock.prelude.numbers]
Z_b2z_1 [lemma, in bedrock.prelude.numbers]
Z_b2z_0 [lemma, in bedrock.prelude.numbers]
Z_b2z_inj [instance, in bedrock.prelude.numbers]
Z_pow2_half [lemma, in bedrock.prelude.numbers]
Z_mod_big [lemma, in bedrock.prelude.numbers]
Z_pow_max_distr_r [lemma, in bedrock.prelude.numbers]
Z_max_add_distr_r [lemma, in bedrock.prelude.numbers]
Z_max_add_distr_l [lemma, in bedrock.prelude.numbers]
Z_land_bit [lemma, in bedrock.prelude.numbers]
Z_ext_iff [lemma, in bedrock.prelude.numbers]
Z_ext [lemma, in bedrock.prelude.numbers]
Z_to_N_max_0 [lemma, in bedrock.prelude.numbers]
Z_of_N_Zto_N_eq_max [lemma, in bedrock.prelude.numbers]
Z_to_N_eq_0_iff [lemma, in bedrock.prelude.numbers]
Z_to_N_eq_0 [lemma, in bedrock.prelude.numbers]
Z_pred_inj [instance, in bedrock.prelude.numbers]
Z_succ_inj [instance, in bedrock.prelude.numbers]
Z_shiftr_right_id [instance, in bedrock.prelude.numbers]
Z_shiftr_left_absorb [instance, in bedrock.prelude.numbers]
Z_shiftl_right_id [instance, in bedrock.prelude.numbers]
Z_shiftl_left_absorb [instance, in bedrock.prelude.numbers]
Z_lor_right_id [instance, in bedrock.prelude.numbers]
Z_lor_left_id [instance, in bedrock.prelude.numbers]
Z_lor_assoc [instance, in bedrock.prelude.numbers]
Z_lor_comm [instance, in bedrock.prelude.numbers]
Z_land_right_absorb [instance, in bedrock.prelude.numbers]
Z_land_left_absorb [instance, in bedrock.prelude.numbers]
Z_land_assoc [instance, in bedrock.prelude.numbers]
Z_land_comm [instance, in bedrock.prelude.numbers]
Z_max_assoc [instance, in bedrock.prelude.numbers]
Z_max_comm [instance, in bedrock.prelude.numbers]
Z_min_assoc [instance, in bedrock.prelude.numbers]
Z_min_comm [instance, in bedrock.prelude.numbers]
Z_trychotomyT [instance, in bedrock.prelude.numbers]
Z_mul_right_absorb [instance, in bedrock.prelude.numbers]
Z_mul_left_absorb [instance, in bedrock.prelude.numbers]
Z_mul_right_id [instance, in bedrock.prelude.numbers]
Z_mul_left_id [instance, in bedrock.prelude.numbers]
Z_mul_comm [instance, in bedrock.prelude.numbers]
Z_mul_assoc [instance, in bedrock.prelude.numbers]
Z_add_right_id [instance, in bedrock.prelude.numbers]
Z_add_left_id [instance, in bedrock.prelude.numbers]
Z_add_comm [instance, in bedrock.prelude.numbers]
Z_add_assoc [instance, in bedrock.prelude.numbers]
Z_comparison [instance, in bedrock.prelude.numbers]
Z_compare [instance, in bedrock.prelude.numbers]
Z2N_inj_divide [lemma, in bedrock.prelude.numbers]
_
_constr [definition, in bedrock.prelude.lens]_constr.inv [variable, in bedrock.prelude.lens]
_constr.constr [variable, in bedrock.prelude.lens]
_constr.B [variable, in bedrock.prelude.lens]
_constr.A2 [variable, in bedrock.prelude.lens]
_constr.A1 [variable, in bedrock.prelude.lens]
_constr [section, in bedrock.prelude.lens]
_apply_unfold [section, in bedrock.prelude.lens]
_total_fun [definition, in bedrock.prelude.lens]
_apply [definition, in bedrock.prelude.lens]
_map_apply [definition, in bedrock.prelude.lens]
_lift [definition, in bedrock.prelude.lens]
_const [definition, in bedrock.prelude.lens]
_snd [definition, in bedrock.prelude.lens]
_fst [definition, in bedrock.prelude.lens]
_id [definition, in bedrock.prelude.lens]
_bit [definition, in bedrock.prelude.lens]
other
[&& _ , _ , .. , _ & _ ] (bool_scope) [notation, in bedrock.prelude.base][&& _ & _ ] (bool_scope) [notation, in bedrock.prelude.base]
_ ==> _ (bool_scope) [notation, in bedrock.prelude.base]
~~ _ (bool_scope) [notation, in bedrock.prelude.base]
(<=) (bool_scope) [notation, in bedrock.prelude.bool]
_ <= _ (bool_scope) [notation, in bedrock.prelude.bool]
_ `with` _ (lens_scope) [notation, in bedrock.prelude.elpi.derive.lens]
_ ≪ _ (N_scope) [notation, in bedrock.prelude.numbers]
_ ≫ _ (N_scope) [notation, in bedrock.prelude.numbers]
_ `ldiff` _ (N_scope) [notation, in bedrock.prelude.numbers]
_ `land` _ (N_scope) [notation, in bedrock.prelude.numbers]
_ `lor` _ (N_scope) [notation, in bedrock.prelude.numbers]
_ <*>@{ _ } _ (stdpp_scope) [notation, in bedrock.prelude.base]
_ <*> _ (stdpp_scope) [notation, in bedrock.prelude.base]
[##ₚ@{ _ } _ ] (stdpp_scope) [notation, in bedrock.prelude.base]
[##ₚ _ ] (stdpp_scope) [notation, in bedrock.prelude.base]
(##ₚ@{ _ } ) (stdpp_scope) [notation, in bedrock.prelude.base]
_ ##ₚ@{ _ } _ (stdpp_scope) [notation, in bedrock.prelude.base]
(.##ₚ _ ) (stdpp_scope) [notation, in bedrock.prelude.base]
( _ ##ₚ.) (stdpp_scope) [notation, in bedrock.prelude.base]
(##ₚ) (stdpp_scope) [notation, in bedrock.prelude.base]
_ ##ₚ _ (stdpp_scope) [notation, in bedrock.prelude.base]
(.@@) (stdpp_scope) [notation, in bedrock.prelude.bytestring]
_ .@@ _ (stdpp_scope) [notation, in bedrock.prelude.bytestring]
let* := _ in _ (stdpp_scope) [notation, in bedrock.prelude.letstar]
let* _ , .. , _ := _ in _ (stdpp_scope) [notation, in bedrock.prelude.letstar]
_ \ _ (stdpp_scope) [notation, in bedrock.prelude.notations]
_ ∖ _ (stdpp_scope) [notation, in bedrock.prelude.notations]
(==@{ _ } ) (stdpp_scope) [notation, in bedrock.prelude.notations]
(.== _ ) (stdpp_scope) [notation, in bedrock.prelude.notations]
( _ ==.) (stdpp_scope) [notation, in bedrock.prelude.notations]
(==) (stdpp_scope) [notation, in bedrock.prelude.notations]
_ ==@{ _ } _ (stdpp_scope) [notation, in bedrock.prelude.notations]
_ == _ (stdpp_scope) [notation, in bedrock.prelude.notations]
_ ~l> _ (type_scope) [notation, in bedrock.prelude.lens]
_ `ldiff` _ (Z_scope) [notation, in bedrock.prelude.numbers]
_ `land` _ (Z_scope) [notation, in bedrock.prelude.numbers]
_ `lor` _ (Z_scope) [notation, in bedrock.prelude.numbers]
[binder _ ] [notation, in bedrock.prelude.named_binder]
π_set [definition, in bedrock.prelude.propset]
Notation Index
B
_ ++ _ (bs_scope) [in bedrock.prelude.bytestring_core]C
_ > _ [in bedrock.prelude.base]_ < _ [in bedrock.prelude.base]
_ == _ [in bedrock.prelude.base]
_ ?= _ [in bedrock.prelude.base]
(?=) [in bedrock.prelude.base]
(.>= _ ) (stdpp_scope) [in bedrock.prelude.base]
( _ >=.) (stdpp_scope) [in bedrock.prelude.base]
(>=@{ _ } ) (stdpp_scope) [in bedrock.prelude.base]
(>=) (stdpp_scope) [in bedrock.prelude.base]
_ >=@{ _ } _ (stdpp_scope) [in bedrock.prelude.base]
_ >= _ (stdpp_scope) [in bedrock.prelude.base]
(.> _ ) (stdpp_scope) [in bedrock.prelude.base]
( _ >.) (stdpp_scope) [in bedrock.prelude.base]
(>@{ _ } ) (stdpp_scope) [in bedrock.prelude.base]
(>) (stdpp_scope) [in bedrock.prelude.base]
_ >@{ _ } _ (stdpp_scope) [in bedrock.prelude.base]
_ > _ (stdpp_scope) [in bedrock.prelude.base]
(.<= _ ) (stdpp_scope) [in bedrock.prelude.base]
( _ <=.) (stdpp_scope) [in bedrock.prelude.base]
(<=@{ _ } ) (stdpp_scope) [in bedrock.prelude.base]
(<=) (stdpp_scope) [in bedrock.prelude.base]
_ <=@{ _ } _ (stdpp_scope) [in bedrock.prelude.base]
_ <= _ (stdpp_scope) [in bedrock.prelude.base]
(.< _ ) (stdpp_scope) [in bedrock.prelude.base]
( _ <.) (stdpp_scope) [in bedrock.prelude.base]
(<@{ _ } ) (stdpp_scope) [in bedrock.prelude.base]
(<) (stdpp_scope) [in bedrock.prelude.base]
_ <@{ _ } _ (stdpp_scope) [in bedrock.prelude.base]
_ < _ (stdpp_scope) [in bedrock.prelude.base]
(.?= _ ) (stdpp_scope) [in bedrock.prelude.base]
( _ ?=.) (stdpp_scope) [in bedrock.prelude.base]
(?=@{ _ } ) (stdpp_scope) [in bedrock.prelude.base]
(?=) (stdpp_scope) [in bedrock.prelude.base]
_ ?=@{ _ } _ (stdpp_scope) [in bedrock.prelude.base]
_ ?= _ (stdpp_scope) [in bedrock.prelude.base]
M
funM _ .. _ => _ (function_scope) [in bedrock.prelude.base]let* := _ in _ (monad_scope) [in bedrock.prelude.base]
let* _ , .. , _ := _ in _ (monad_scope) [in bedrock.prelude.base]
(>>=) (stdpp_scope) [in bedrock.prelude.base]
(.>>= _ ) (stdpp_scope) [in bedrock.prelude.base]
( _ >>=.) (stdpp_scope) [in bedrock.prelude.base]
_ >>=@{ _ } _ (stdpp_scope) [in bedrock.prelude.base]
_ ≫= _ (stdpp_scope) [in bedrock.prelude.base]
_ >>= _ (stdpp_scope) [in bedrock.prelude.base]
letM* := _ in _ (stdpp_scope) [in bedrock.prelude.base]
letM* _ , .. , _ := _ in _ (stdpp_scope) [in bedrock.prelude.base]
W
_ <= _ (Qp_scope) [in bedrock.prelude.numbers]_ + _ (wrapN_scope) [in bedrock.prelude.wrap]
0 (wrapN_scope) [in bedrock.prelude.wrap]
other
[&& _ , _ , .. , _ & _ ] (bool_scope) [in bedrock.prelude.base][&& _ & _ ] (bool_scope) [in bedrock.prelude.base]
_ ==> _ (bool_scope) [in bedrock.prelude.base]
~~ _ (bool_scope) [in bedrock.prelude.base]
(<=) (bool_scope) [in bedrock.prelude.bool]
_ <= _ (bool_scope) [in bedrock.prelude.bool]
_ `with` _ (lens_scope) [in bedrock.prelude.elpi.derive.lens]
_ ≪ _ (N_scope) [in bedrock.prelude.numbers]
_ ≫ _ (N_scope) [in bedrock.prelude.numbers]
_ `ldiff` _ (N_scope) [in bedrock.prelude.numbers]
_ `land` _ (N_scope) [in bedrock.prelude.numbers]
_ `lor` _ (N_scope) [in bedrock.prelude.numbers]
_ <*>@{ _ } _ (stdpp_scope) [in bedrock.prelude.base]
_ <*> _ (stdpp_scope) [in bedrock.prelude.base]
[##ₚ@{ _ } _ ] (stdpp_scope) [in bedrock.prelude.base]
[##ₚ _ ] (stdpp_scope) [in bedrock.prelude.base]
(##ₚ@{ _ } ) (stdpp_scope) [in bedrock.prelude.base]
_ ##ₚ@{ _ } _ (stdpp_scope) [in bedrock.prelude.base]
(.##ₚ _ ) (stdpp_scope) [in bedrock.prelude.base]
( _ ##ₚ.) (stdpp_scope) [in bedrock.prelude.base]
(##ₚ) (stdpp_scope) [in bedrock.prelude.base]
_ ##ₚ _ (stdpp_scope) [in bedrock.prelude.base]
(.@@) (stdpp_scope) [in bedrock.prelude.bytestring]
_ .@@ _ (stdpp_scope) [in bedrock.prelude.bytestring]
let* := _ in _ (stdpp_scope) [in bedrock.prelude.letstar]
let* _ , .. , _ := _ in _ (stdpp_scope) [in bedrock.prelude.letstar]
_ \ _ (stdpp_scope) [in bedrock.prelude.notations]
_ ∖ _ (stdpp_scope) [in bedrock.prelude.notations]
(==@{ _ } ) (stdpp_scope) [in bedrock.prelude.notations]
(.== _ ) (stdpp_scope) [in bedrock.prelude.notations]
( _ ==.) (stdpp_scope) [in bedrock.prelude.notations]
(==) (stdpp_scope) [in bedrock.prelude.notations]
_ ==@{ _ } _ (stdpp_scope) [in bedrock.prelude.notations]
_ == _ (stdpp_scope) [in bedrock.prelude.notations]
_ ~l> _ (type_scope) [in bedrock.prelude.lens]
_ `ldiff` _ (Z_scope) [in bedrock.prelude.numbers]
_ `land` _ (Z_scope) [in bedrock.prelude.numbers]
_ `lor` _ (Z_scope) [in bedrock.prelude.numbers]
[binder _ ] [in bedrock.prelude.named_binder]
Module Index
A
Alias [in bedrock.prelude.elpi.derive_test]Alias.Cmd [in bedrock.prelude.elpi.derive_test]
Alias.Countable [in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasDirect [in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasIndirect [in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnVariant [in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnAliasIndirect [in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnAliasDirect [in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnVariant [in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec [in bedrock.prelude.elpi.derive_test]
Alias.Finite [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant [in bedrock.prelude.elpi.derive_test]
Alias.Inhabited [in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnAliasDirect [in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnAliasIndirect [in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnVariant [in bedrock.prelude.elpi.derive_test]
attrs [in bedrock.prelude.page]
B
BasicTests [in bedrock.prelude.elpi.derive_test]Binder [in bedrock.prelude.named_binder]
bitmask_type_simple_mixin [in bedrock.prelude.finite]
bitmask_type [in bedrock.prelude.finite]
BitsetTest [in bedrock.prelude.elpi.derive_test]
BitsetTest.feature [in bedrock.prelude.elpi.derive_test]
BitsetTest.feature_set [in bedrock.prelude.elpi.derive_test]
Bool [in bedrock.prelude.bool]
BS [in bedrock.prelude.bytestring]
BS [in bedrock.prelude.bytestring_core]
BS.Buf [in bedrock.prelude.bytestring_core]
BS.Bytestring_notations [in bedrock.prelude.bytestring_core]
C
compare [in bedrock.prelude.base]compare.Notations [in bedrock.prelude.base]
Compose [in bedrock.prelude.sts]
cpu [in bedrock.prelude.hw_types]
D
DerivingTest [in bedrock.prelude.elpi.derive_test]Deriving2Test [in bedrock.prelude.elpi.derive_test]
E
eqdec_type [in bedrock.prelude.finite]Error [in bedrock.prelude.error]
ERROR [in bedrock.prelude.error]
F
fin [in bedrock.prelude.fin]FiniteTest [in bedrock.prelude.elpi.derive_test]
FiniteTest.feature [in bedrock.prelude.elpi.derive_test]
finite_bits [in bedrock.prelude.finite]
finite_bits_aux.internal [in bedrock.prelude.finite]
finite_bits_aux [in bedrock.prelude.finite]
finite_bitmask_type_intf [in bedrock.prelude.finite]
finite_bitmask_type_mixin [in bedrock.prelude.finite]
finite_type_intf [in bedrock.prelude.finite]
finite_type_mixin [in bedrock.prelude.finite]
finite_encoded_type_mixin [in bedrock.prelude.finite]
finite_encoded_type [in bedrock.prelude.finite]
finite_type [in bedrock.prelude.finite]
fin_prod.internal [in bedrock.prelude.finite_prod]
fin_prod [in bedrock.prelude.finite_prod]
FMapExtra [in bedrock.prelude.avl]
FMapExtra.LEIBNIZ_EQ [in bedrock.prelude.avl]
FMapExtra.MAP [in bedrock.prelude.avl]
FMapExtra.MAP.Raw [in bedrock.prelude.avl]
FMapExtra.MIXIN [in bedrock.prelude.avl]
FMapExtra.MIXIN_LEIBNIZ [in bedrock.prelude.avl]
FMapExtra.RAW [in bedrock.prelude.avl]
FMapExtra.RAW.Proofs [in bedrock.prelude.avl]
FMapExtra.RAW.Proofs.MX [in bedrock.prelude.avl]
I
IM [in bedrock.prelude.avl]InteropTests [in bedrock.prelude.elpi.derive_test]
int_line [in bedrock.prelude.hw_types]
iso [in bedrock.prelude.lens]
L
lens_aux_1.lens [in bedrock.prelude.lens]lens_aux_1 [in bedrock.prelude.lens]
M
mmio_idx [in bedrock.prelude.hw_types]MonadNotations [in bedrock.prelude.base]
O
on_props [in bedrock.prelude.option]option [in bedrock.prelude.option]
OT_bs [in bedrock.prelude.bytestring_core]
OT_byte [in bedrock.prelude.bytestring_core]
P
Pos [in bedrock.prelude.numbers]Q
Qp [in bedrock.prelude.numbers]S
SimpleBitsetTest [in bedrock.prelude.elpi.derive_test]SimpleBitsetTest.feature [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature_set [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature [in bedrock.prelude.elpi.derive_test]
simple_finite_bits [in bedrock.prelude.finite]
simple_finite_bits_aux [in bedrock.prelude.finite]
simple_finite_bitmask_type_intf [in bedrock.prelude.finite]
simple_finite_bitmask_type_mixin [in bedrock.prelude.finite]
size_bytes [in bedrock.prelude.hw_types]
some_Forall2 [in bedrock.prelude.option]
some_Forall2_Locked [in bedrock.prelude.option]
Sts [in bedrock.prelude.sts]
succ_wrapper [in bedrock.prelude.wrap]
sum [in bedrock.prelude.sum]
T
TEST [in bedrock.prelude.list]Test [in bedrock.prelude.named_binder]
Test [in bedrock.prelude.fin]
time [in bedrock.prelude.hw_types]
TO_UPSTREAM_TRANSPARENT [in bedrock.prelude.fin]
types [in bedrock.prelude.hw_types]
W
wrapN_notations [in bedrock.prelude.wrap]wrapper [in bedrock.prelude.wrap]
Variable Index
A
ap.A [in bedrock.prelude.list]ap.B [in bedrock.prelude.list]
ap.C [in bedrock.prelude.list]
C
char_parsec.MB [in bedrock.prelude.parsec]char_parsec.FM [in bedrock.prelude.parsec]
char_parsec.MR [in bedrock.prelude.parsec]
char_parsec.F [in bedrock.prelude.parsec]
Compose.Compose.sf [in bedrock.prelude.sts]
Compose.Compose.sf [in bedrock.prelude.sts]
D
dep_fn_insert.T [in bedrock.prelude.functions]dep_fn_insert.A [in bedrock.prelude.functions]
Deriving2Test.test.x [in bedrock.prelude.elpi.derive_test]
dom_map_seqZ.HF [in bedrock.prelude.fin_map_dom]
dom_map_seqZ.HP [in bedrock.prelude.fin_map_dom]
dom_map_seqZ.HE [in bedrock.prelude.fin_map_dom]
dom_map_seqZ.HL [in bedrock.prelude.fin_map_dom]
E
enc_finite_N.to_of_N [in bedrock.prelude.finite]enc_finite_N.to_N_c [in bedrock.prelude.finite]
enc_finite_N.of_to_N [in bedrock.prelude.finite]
enc_finite_N.c [in bedrock.prelude.finite]
enc_finite_N.of_N [in bedrock.prelude.finite]
enc_finite_N.to_N [in bedrock.prelude.finite]
enc_finite.to_of_nat [in bedrock.prelude.finite]
enc_finite.to_nat_c [in bedrock.prelude.finite]
enc_finite.of_to_nat [in bedrock.prelude.finite]
enc_finite.c [in bedrock.prelude.finite]
enc_finite.of_nat [in bedrock.prelude.finite]
enc_finite.to_nat [in bedrock.prelude.finite]
F
finite_bits_aux.BT_to_bit_inj.Hinj [in bedrock.prelude.finite]finite_bitmask_type_mixin.to_bit_inj.Hinj [in bedrock.prelude.finite]
finite_preimage.finite_preimage_inj.Hinj [in bedrock.prelude.finite]
fin_map_dom.A [in bedrock.prelude.fin_map_dom]
fin_prod.internal.theory_with_fg.ns [in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_fg.B [in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_fg.A [in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_eq_dec.ns [in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_eq_dec.A [in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_type.A [in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_type.name [in bedrock.prelude.finite_prod]
fin_prod.internal.with_eq_dec.A [in bedrock.prelude.finite_prod]
fin_prod.internal.with_fg.B [in bedrock.prelude.finite_prod]
fin_prod.internal.with_fg.A [in bedrock.prelude.finite_prod]
fin_prod.internal.with_fg.name [in bedrock.prelude.finite_prod]
fin_maps.A [in bedrock.prelude.fin_maps]
flip_app.A [in bedrock.prelude.base]
FMapExtra.MIXIN.canon.A [in bedrock.prelude.avl]
FMapExtra.MIXIN.map.A [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw.A [in bedrock.prelude.avl]
FMapExtra.RAW.bst.elt [in bedrock.prelude.avl]
FMapExtra.RAW.ops.add [in bedrock.prelude.avl]
FMapExtra.RAW.ops.bal [in bedrock.prelude.avl]
FMapExtra.RAW.ops.cardinal [in bedrock.prelude.avl]
FMapExtra.RAW.ops.concat [in bedrock.prelude.avl]
FMapExtra.RAW.ops.create [in bedrock.prelude.avl]
FMapExtra.RAW.ops.elements [in bedrock.prelude.avl]
FMapExtra.RAW.ops.elements_aux [in bedrock.prelude.avl]
FMapExtra.RAW.ops.elt [in bedrock.prelude.avl]
FMapExtra.RAW.ops.empty [in bedrock.prelude.avl]
FMapExtra.RAW.ops.equal [in bedrock.prelude.avl]
FMapExtra.RAW.ops.find [in bedrock.prelude.avl]
FMapExtra.RAW.ops.fold [in bedrock.prelude.avl]
FMapExtra.RAW.ops.height [in bedrock.prelude.avl]
FMapExtra.RAW.ops.is_empty [in bedrock.prelude.avl]
FMapExtra.RAW.ops.join [in bedrock.prelude.avl]
FMapExtra.RAW.ops.mem [in bedrock.prelude.avl]
FMapExtra.RAW.ops.merge [in bedrock.prelude.avl]
FMapExtra.RAW.ops.remove [in bedrock.prelude.avl]
FMapExtra.RAW.ops.remove_min [in bedrock.prelude.avl]
FMapExtra.RAW.ops.split [in bedrock.prelude.avl]
G
get_range_bitsN.get_range_bitsN_bounded_elim.from [in bedrock.prelude.bitsN]get_range_bitsN.get_range_bitsN_bounded_elim.n [in bedrock.prelude.bitsN]
get_range_bitsN.get_range_bitsN_bounded_elim.count [in bedrock.prelude.bitsN]
get_range_bitsN.get_range_bitsN_bounded_elim.of_N [in bedrock.prelude.bitsN]
get_range_bitsN.get_range_bitsN_bounded_elim.X [in bedrock.prelude.bitsN]
L
listN.A [in bedrock.prelude.list_numbers]lists.A [in bedrock.prelude.list]
lists.B [in bedrock.prelude.list]
lists.zip_with.C [in bedrock.prelude.list]
list.A [in bedrock.prelude.list]
M
monoid.A [in bedrock.prelude.lens]N
NoDup_fmap_ap.C [in bedrock.prelude.list]NoDup_fmap_ap.B [in bedrock.prelude.list]
NoDup_fmap_ap.A [in bedrock.prelude.list]
NoDup_ap.C [in bedrock.prelude.list]
NoDup_ap.B [in bedrock.prelude.list]
NoDup_ap.A [in bedrock.prelude.list]
O
on_props.on_props.f [in bedrock.prelude.option]on_props.on_props.B [in bedrock.prelude.option]
on_props.on_props.A [in bedrock.prelude.option]
Q
Qp.Qp_all.C [in bedrock.prelude.numbers]R
Roption_leq.A [in bedrock.prelude.option]S
same_property.obs [in bedrock.prelude.option]seqW.Phant [in bedrock.prelude.wrap]
set_map_functorial.compose.g [in bedrock.prelude.fin_sets]
set_map_functorial.compose.f [in bedrock.prelude.fin_sets]
some_Forall2_eq.A [in bedrock.prelude.option]
some_Forall2.R [in bedrock.prelude.option]
Sts.hide.L [in bedrock.prelude.sts]
Sts.hide.P [in bedrock.prelude.sts]
Sts.map.f [in bedrock.prelude.sts]
Sts.map.L [in bedrock.prelude.sts]
Sts.map.L' [in bedrock.prelude.sts]
Sts.map.STS [in bedrock.prelude.sts]
Sts.par.dual [in bedrock.prelude.sts]
Sts.par.e [in bedrock.prelude.sts]
Sts.par.L [in bedrock.prelude.sts]
Sts.par.R [in bedrock.prelude.sts]
T
TO_UPSTREAM_TRANSPARENT.dsig_transparent.P [in bedrock.prelude.fin]TO_UPSTREAM_TRANSPARENT.dsig_transparent.A [in bedrock.prelude.fin]
U
under_proper.R [in bedrock.prelude.under_rel_proper]under_proper.T [in bedrock.prelude.under_rel_proper]
_
_constr.inv [in bedrock.prelude.lens]_constr.constr [in bedrock.prelude.lens]
_constr.B [in bedrock.prelude.lens]
_constr.A2 [in bedrock.prelude.lens]
_constr.A1 [in bedrock.prelude.lens]
Library Index
A
addravl
B
basebase_dbs
basis
bitset
bitsN
bool
bytestring
bytestring_core
C
commoncompare
countable
D
derivederive_test
dummy
E
eq_decerror
F
finfinite
finite
finite_type
finite_prod
fin_sets
fin_map_dom
fin_maps
functions
funext
G
gmapH
hw_typesI
inhabitedinterrupts
L
lenslens
letstar
list
listset_nodup
list_numbers
N
namenamed_binder
notations
numbers
O
optionP
pageparsec
prelude
proper
propset
R
relationsreserved_notation
S
setsstdpp_ssreflect
sts
sum
T
tc_cond_typetelescopes
telescopes
U
under_rel_properW
wrapLemma Index
A
align_up_nonneg [in bedrock.prelude.numbers]align_dn_nonneg [in bedrock.prelude.numbers]
align_dn_le_up [in bedrock.prelude.numbers]
align_up_mono [in bedrock.prelude.numbers]
align_up_above [in bedrock.prelude.numbers]
align_up_below [in bedrock.prelude.numbers]
align_up_divide [in bedrock.prelude.numbers]
align_dn_mono [in bedrock.prelude.numbers]
align_dn_above [in bedrock.prelude.numbers]
align_dn_below [in bedrock.prelude.numbers]
align_dn_divide [in bedrock.prelude.numbers]
align_dn_pow2 [in bedrock.prelude.numbers]
alterN_explode [in bedrock.prelude.list_numbers]
andP [in bedrock.prelude.bool]
and_proper_r [in bedrock.prelude.base]
and_proper_l [in bedrock.prelude.base]
ap_app_r [in bedrock.prelude.list]
ap_app_l [in bedrock.prelude.list]
ap_cons_r_p [in bedrock.prelude.list]
ap_cons_l [in bedrock.prelude.list]
ap_nil_r [in bedrock.prelude.list]
ap_nil_l [in bedrock.prelude.list]
B
bitmask_type_simple_mixin.to_bit_lt_card_N [in bedrock.prelude.finite]bitmask_type_simple_mixin.to_of_bit [in bedrock.prelude.finite]
bitmask_type_simple_mixin.of_to_bit [in bedrock.prelude.finite]
boolP [in bedrock.prelude.bool]
bool_decide_lt_irrefl [in bedrock.prelude.list_numbers]
bool_decide_sub_move_0_r [in bedrock.prelude.list_numbers]
bool_decide_refl [in bedrock.prelude.list_numbers]
bool_decide_is_true [in bedrock.prelude.bool]
bool_decide_bool_eq [in bedrock.prelude.bool]
bool_decide_Is_true [in bedrock.prelude.bool]
Bool.andb_min_r [in bedrock.prelude.bool]
Bool.andb_min_l [in bedrock.prelude.bool]
Bool.le_andb_r [in bedrock.prelude.bool]
Bool.le_andb_l [in bedrock.prelude.bool]
Bool.le_leb [in bedrock.prelude.bool]
BS.append_alt [in bedrock.prelude.bytestring_core]
BS.of_string_to_string_inv [in bedrock.prelude.bytestring]
BS.parse_string_inv [in bedrock.prelude.bytestring_core]
BS.parse_nil_inv [in bedrock.prelude.bytestring_core]
BS.parse_cons [in bedrock.prelude.bytestring_core]
BS.parse_nil [in bedrock.prelude.bytestring_core]
BS.parse_print_inv [in bedrock.prelude.bytestring_core]
BS.print_length [in bedrock.prelude.bytestring_core]
BS.print_append [in bedrock.prelude.bytestring_core]
BS.print_append_tailrec [in bedrock.prelude.bytestring_core]
BS.print_rev [in bedrock.prelude.bytestring_core]
BS.print_rev_append [in bedrock.prelude.bytestring_core]
BS.print_cons_inv [in bedrock.prelude.bytestring_core]
BS.print_nil_inv [in bedrock.prelude.bytestring_core]
BS.print_string [in bedrock.prelude.bytestring_core]
BS.print_empty [in bedrock.prelude.bytestring_core]
BS.print_parse_inv [in bedrock.prelude.bytestring_core]
BS.rev_app [in bedrock.prelude.bytestring_core]
BS.rev_involutive [in bedrock.prelude.bytestring_core]
BS.rev_string [in bedrock.prelude.bytestring_core]
BS.rev_empty [in bedrock.prelude.bytestring_core]
BS.to_string_of_string_inv [in bedrock.prelude.bytestring]
byte_cmp_spec [in bedrock.prelude.bytestring_core]
byte_to_N_inj [in bedrock.prelude.bytestring_core]
byte_cmp_refl [in bedrock.prelude.bytestring_core]
C
cancel_MkwrapN [in bedrock.prelude.wrap]cancel_unwrapN [in bedrock.prelude.wrap]
compare.compare [in bedrock.prelude.base]
compare.compare_spec [in bedrock.prelude.base]
Compose.dual_sets_singletons [in bedrock.prelude.sts]
Compose.step_star_ext_lift_single [in bedrock.prelude.sts]
Compose.step_star_tau_lift [in bedrock.prelude.sts]
constr_laws [in bedrock.prelude.lens]
constr_set_set [in bedrock.prelude.lens]
constr_set_view [in bedrock.prelude.lens]
constr_view_set [in bedrock.prelude.lens]
constr_view_over [in bedrock.prelude.lens]
cons_seqW' [in bedrock.prelude.wrap]
cons_seqW [in bedrock.prelude.wrap]
cons_seqN [in bedrock.prelude.list_numbers]
contraNN [in bedrock.prelude.bool]
D
decode_N_is_inverse [in bedrock.prelude.finite]decode_N_None_encode_N [in bedrock.prelude.finite]
decode_N_encode_N [in bedrock.prelude.finite]
decode_N_Some_encode_N [in bedrock.prelude.finite]
decode_N_nat [in bedrock.prelude.finite]
decode_nat_N [in bedrock.prelude.finite]
decode_encode_N [in bedrock.prelude.finite]
dec_stable_iff [in bedrock.prelude.base]
dep_fn_insert_exchange_fun [in bedrock.prelude.functions]
dep_fn_insert_set_set_fun [in bedrock.prelude.functions]
dep_fn_insert_set_view_fun [in bedrock.prelude.functions]
dep_fn_insert_exchange [in bedrock.prelude.functions]
dep_fn_insert_set_set [in bedrock.prelude.functions]
dep_fn_insert_set_view [in bedrock.prelude.functions]
dep_fn_insert_view_set_ne [in bedrock.prelude.functions]
dep_fn_insert_view_set' [in bedrock.prelude.functions]
dep_fn_insert_view_set [in bedrock.prelude.functions]
difference_map_disjoint [in bedrock.prelude.fin_maps]
disjoint_cons_r [in bedrock.prelude.list]
dom_seqZ_L [in bedrock.prelude.fin_map_dom]
dom_seqZ [in bedrock.prelude.fin_map_dom]
dropN_sliceZ [in bedrock.prelude.list_numbers]
dropN_congr [in bedrock.prelude.list_numbers]
dropN_insertN_lt [in bedrock.prelude.list_numbers]
dropN_insertN_ge [in bedrock.prelude.list_numbers]
dropN_lookupN [in bedrock.prelude.list_numbers]
dropN_resizeN_le [in bedrock.prelude.list_numbers]
dropN_resizeN_plus [in bedrock.prelude.list_numbers]
dropN_takeN [in bedrock.prelude.list_numbers]
dropN_app [in bedrock.prelude.list_numbers]
dropN_cons_succ [in bedrock.prelude.list_numbers]
dropN_nil [in bedrock.prelude.list_numbers]
dropN_dropN [in bedrock.prelude.list_numbers]
dropN_tail [in bedrock.prelude.list_numbers]
dropN_one [in bedrock.prelude.list_numbers]
dropN_zero [in bedrock.prelude.list_numbers]
dropN_lengthN [in bedrock.prelude.list_numbers]
dropN_replicateN_succ [in bedrock.prelude.list_numbers]
dropN_replicateN_plus [in bedrock.prelude.list_numbers]
dropN_replicateN [in bedrock.prelude.list_numbers]
dropN_seqN_cons [in bedrock.prelude.list_numbers]
dropN_seqN [in bedrock.prelude.list_numbers]
E
elements_set_seq [in bedrock.prelude.fin_sets]elements_set_equiv_L [in bedrock.prelude.fin_sets]
elements_set_equiv_1 [in bedrock.prelude.fin_sets]
elem_of_map_to_list_dom [in bedrock.prelude.fin_map_dom]
elem_of_list_fmap_ap [in bedrock.prelude.list]
elem_of_list_ap [in bedrock.prelude.list]
elem_of_zip [in bedrock.prelude.list]
elem_of_rangeZ [in bedrock.prelude.list_numbers]
elem_of_replicateN [in bedrock.prelude.list_numbers]
elem_of_seqN [in bedrock.prelude.list_numbers]
elem_of_set_rangeZ [in bedrock.prelude.fin_sets]
elem_of_set_concat_map [in bedrock.prelude.fin_sets]
elem_of_gset_bind [in bedrock.prelude.gmap]
elem_of_app_fmap_enum_l [in bedrock.prelude.finite]
elem_of_finite_preimage_set [in bedrock.prelude.finite]
elem_of_finite_preimage [in bedrock.prelude.finite]
elem_of_filter_enum [in bedrock.prelude.finite]
elem_of_enum' [in bedrock.prelude.finite]
elimT [in bedrock.prelude.bool]
encode_decode_N [in bedrock.prelude.finite]
encode_N_lt_card_N [in bedrock.prelude.finite]
encode_N_nat [in bedrock.prelude.finite]
encode_nat_N [in bedrock.prelude.finite]
enc_finite_enum [in bedrock.prelude.finite]
enum_lookup_encode_N [in bedrock.prelude.finite]
enum_lookup_encode_nat [in bedrock.prelude.finite]
F
finite_bits_aux.to_bits_inv_singleton_ne_Z [in bedrock.prelude.finite]finite_bits_aux.to_bits_inv_singleton_Z [in bedrock.prelude.finite]
finite_bits_aux.to_bits_inv_singleton_ne [in bedrock.prelude.finite]
finite_bits_aux.to_bits_inv_singleton [in bedrock.prelude.finite]
finite_bits_aux.to_of_bits [in bedrock.prelude.finite]
finite_bits_aux.N_testbit_mask_top_to_bit [in bedrock.prelude.finite]
finite_bits_aux.N_testbit_to_bits [in bedrock.prelude.finite]
finite_bits_aux.elem_of_masked [in bedrock.prelude.finite]
finite_bits_aux.masked_opt_top [in bedrock.prelude.finite]
finite_bits_aux.masked_top [in bedrock.prelude.finite]
finite_bits_aux.masked_opt_empty [in bedrock.prelude.finite]
finite_bits_aux.masked_empty [in bedrock.prelude.finite]
finite_bits_aux.masked_opt_0 [in bedrock.prelude.finite]
finite_bits_aux.masked_0 [in bedrock.prelude.finite]
finite_bits_aux.of_bits_singleton [in bedrock.prelude.finite]
finite_bits_aux.of_to_bits [in bedrock.prelude.finite]
finite_bits_aux.of_bits_setbit [in bedrock.prelude.finite]
finite_bits_aux.to_bits_intersection [in bedrock.prelude.finite]
finite_bits_aux.to_bits_intersection_singleton [in bedrock.prelude.finite]
finite_bits_aux.to_bitmask_land_neq [in bedrock.prelude.finite]
finite_bits_aux.to_bits_union [in bedrock.prelude.finite]
finite_bits_aux.to_bits_union_singleton [in bedrock.prelude.finite]
finite_bits_aux.setbit_in_idemp [in bedrock.prelude.finite]
finite_bits_aux.to_bits_union_singleton_aux [in bedrock.prelude.finite]
finite_bits_aux.internal.to_bits_is_comm [in bedrock.prelude.finite]
finite_bits_aux.internal.to_bits_is_alt [in bedrock.prelude.finite]
finite_bits_aux.to_bits_singleton [in bedrock.prelude.finite]
finite_bits_aux.to_bits_empty [in bedrock.prelude.finite]
finite_bits_aux.of_bits_and [in bedrock.prelude.finite]
finite_bits_aux.of_bits_or [in bedrock.prelude.finite]
finite_bits_aux.of_bits_0 [in bedrock.prelude.finite]
finite_bits_aux.elem_of_of_bits [in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_list_setbit [in bedrock.prelude.finite]
finite_bitmask_type_mixin.filter_setbit [in bedrock.prelude.finite]
finite_bitmask_type_mixin.filter_setbit' [in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_to_bitmask_inj [in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_setbit_inj [in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_to_bitmask_eq [in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_to_bitmask [in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_setbit [in bedrock.prelude.finite]
finite_bitmask_type_mixin.setbit_is_alt [in bedrock.prelude.finite]
finite_bitmask_type_mixin.setbit_0 [in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_to_list_and [in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_to_list_or [in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_to_list_0 [in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_list_0 [in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_to_list [in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_filter_land [in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_filter_lor [in bedrock.prelude.finite]
finite_bitmask_type_mixin.filter_0 [in bedrock.prelude.finite]
finite_bitmask_type_mixin.elem_of_filter [in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_land [in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_lor [in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit_0 [in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_bitmask_setbit [in bedrock.prelude.finite]
finite_type_mixin.to_N_lt_card_N [in bedrock.prelude.finite]
finite_type_mixin.to_of_N [in bedrock.prelude.finite]
finite_type_mixin.of_to_N [in bedrock.prelude.finite]
finite_encoded_type_mixin.to_of_N [in bedrock.prelude.finite]
finite_encoded_type_mixin.of_to_N [in bedrock.prelude.finite]
finite_decode_N_lt [in bedrock.prelude.finite]
finite_decode_N_unfold [in bedrock.prelude.finite]
finite_decode_N_unfold' [in bedrock.prelude.finite]
finite_decode_nat_lt [in bedrock.prelude.finite]
finite_decode_nat_unfold [in bedrock.prelude.finite]
finite_preimage_set_inj_singleton_L [in bedrock.prelude.finite]
finite_preimage_set_singleton_L [in bedrock.prelude.finite]
finite_preimage_set_union_L [in bedrock.prelude.finite]
finite_preimage_set_empty_L [in bedrock.prelude.finite]
finite_preimage_set_inj_singleton [in bedrock.prelude.finite]
finite_preimage_set_singleton [in bedrock.prelude.finite]
finite_preimage_set_union [in bedrock.prelude.finite]
finite_preimage_set_empty [in bedrock.prelude.finite]
finite_inverse_inj_Some_equiv [in bedrock.prelude.finite]
finite_inverse_inj_cancel [in bedrock.prelude.finite]
finite_inverse_None_equiv [in bedrock.prelude.finite]
finite_inverse_is_Some [in bedrock.prelude.finite]
finite_inverse_Some_inv [in bedrock.prelude.finite]
finite_preimage_inj_singleton [in bedrock.prelude.finite]
fin_prod.lookup_ext [in bedrock.prelude.finite_prod]
fin_prod.lookup_update_ne [in bedrock.prelude.finite_prod]
fin_prod.lookup_update_eq [in bedrock.prelude.finite_prod]
fin_prod.fmapO_None [in bedrock.prelude.finite_prod]
fin_prod.fmapO_Some [in bedrock.prelude.finite_prod]
fin_prod.lookup_fmap [in bedrock.prelude.finite_prod]
fin_prod.lookup_unfold [in bedrock.prelude.finite_prod]
fin_prod.internal.fmapO'_None [in bedrock.prelude.finite_prod]
fin_prod.internal.fmapO'_Some_1 [in bedrock.prelude.finite_prod]
fin_prod.internal.fmapO'_Some [in bedrock.prelude.finite_prod]
fin_prod.internal.lookup_fmap' [in bedrock.prelude.finite_prod]
fin_prod.internal.lookup'_ext [in bedrock.prelude.finite_prod]
fin_prod.internal.lookup_update'_ne [in bedrock.prelude.finite_prod]
fin_prod.internal.lookup_update'_eq [in bedrock.prelude.finite_prod]
fin_prod.internal.lookup'_elem_of_Some [in bedrock.prelude.finite_prod]
fin_prod.internal.to_list'_cons [in bedrock.prelude.finite_prod]
fin_prod.internal.to_list'_nil [in bedrock.prelude.finite_prod]
fin_fun_eq_refl_transport [in bedrock.prelude.finite]
fin_fun_eq_refl [in bedrock.prelude.finite]
fin_fun_decide_True_pi [in bedrock.prelude.finite]
fin.elem_of_seq [in bedrock.prelude.fin]
fin.enum_unfold [in bedrock.prelude.fin]
fin.is_succ [in bedrock.prelude.fin]
fin.is_zero [in bedrock.prelude.fin]
fin.is_mk [in bedrock.prelude.fin]
fin.of_to_idx_fin_cancel [in bedrock.prelude.fin]
fin.of_to_N [in bedrock.prelude.fin]
fin.of_to_N' [in bedrock.prelude.fin]
fin.proj1_sig_of_N [in bedrock.prelude.fin]
fin.seq_lookupN [in bedrock.prelude.fin]
fin.seq_NoDup [in bedrock.prelude.fin]
fin.seq_len [in bedrock.prelude.fin]
fin.seq_lenN [in bedrock.prelude.fin]
fin.to_of_idx_fin_cancel [in bedrock.prelude.fin]
fin.to_of_N_gt [in bedrock.prelude.fin]
fin.to_of_N [in bedrock.prelude.fin]
fin.to_of_N_gt' [in bedrock.prelude.fin]
fin.to_of_N' [in bedrock.prelude.fin]
fin.to_N_lt [in bedrock.prelude.fin]
fin.t_rect [in bedrock.prelude.fin]
fin.t_sig_rect [in bedrock.prelude.fin]
fin.t_gt_inhabited [in bedrock.prelude.fin]
fin.t_inv [in bedrock.prelude.fin]
fin.t_0_inv [in bedrock.prelude.fin]
flip_assoc [in bedrock.prelude.base]
FMapExtra.MIXIN_LEIBNIZ.find_any_ok [in bedrock.prelude.avl]
FMapExtra.MIXIN_LEIBNIZ.map_to_list_elements [in bedrock.prelude.avl]
FMapExtra.MIXIN.check_canon_ok [in bedrock.prelude.avl]
FMapExtra.MIXIN.check_canonP [in bedrock.prelude.avl]
fmap_ext_in [in bedrock.prelude.list]
fmap_S_seqN [in bedrock.prelude.list_numbers]
fmap_add_seqN_0 [in bedrock.prelude.list_numbers]
fmap_add_seqN [in bedrock.prelude.list_numbers]
fmap_dropN [in bedrock.prelude.list_numbers]
fmap_lengthN [in bedrock.prelude.list_numbers]
fmap_add_seq_0 [in bedrock.prelude.list_numbers]
fn_lookup_total_unfold [in bedrock.prelude.functions]
foldl_left [in bedrock.prelude.list]
foldl_rev [in bedrock.prelude.list]
foldr_rev [in bedrock.prelude.list]
foldr_cons [in bedrock.prelude.list]
fold_left_cons [in bedrock.prelude.avl]
Forall_fmap_fmap [in bedrock.prelude.list]
Forall_fmap_fmap_1 [in bedrock.prelude.list]
Forall_seqN [in bedrock.prelude.list_numbers]
Forall2_symmetric_strong [in bedrock.prelude.list]
funext_equiv [in bedrock.prelude.axioms.funext]
G
get_range_bitsN_bounded_elim' [in bedrock.prelude.bitsN]get_range_bitsN_bounded_elim [in bedrock.prelude.bitsN]
get_range_bitsN_bounded [in bedrock.prelude.bitsN]
get_range_bitsN_1_bool_decide_eq [in bedrock.prelude.bitsN]
get_range_bitsN_1_eq [in bedrock.prelude.bitsN]
get_range_bitsN_eq [in bedrock.prelude.bitsN]
gset_bind_singleton [in bedrock.prelude.gmap]
gset_bind_union [in bedrock.prelude.gmap]
gset_bind_empty [in bedrock.prelude.gmap]
gset_eq [in bedrock.prelude.gmap]
H
head_Some_elem_of [in bedrock.prelude.list]head_list_take [in bedrock.prelude.list_numbers]
I
iff_forall [in bedrock.prelude.base]implb_prop_elim [in bedrock.prelude.bool]
implb_prop_intro [in bedrock.prelude.bool]
implb_True [in bedrock.prelude.bool]
implyP [in bedrock.prelude.bool]
IM.eqL [in bedrock.prelude.avl]
inj2_iff [in bedrock.prelude.base]
insertN_takeN_dropN [in bedrock.prelude.list_numbers]
insertN_explode [in bedrock.prelude.list_numbers]
insertN_replicateN [in bedrock.prelude.list_numbers]
insertN_app_r [in bedrock.prelude.list_numbers]
insertN_app_l [in bedrock.prelude.list_numbers]
insertN_comm [in bedrock.prelude.list_numbers]
insertN_insertN [in bedrock.prelude.list_numbers]
insertN_lengthN [in bedrock.prelude.list_numbers]
insertN_cons_succ [in bedrock.prelude.list_numbers]
insertN_cons_zero [in bedrock.prelude.list_numbers]
insertN_nil [in bedrock.prelude.list_numbers]
insertN_id [in bedrock.prelude.list_numbers]
insertN_seqN [in bedrock.prelude.list_numbers]
insertZ_preserves_sliceZ [in bedrock.prelude.list_numbers]
insertZ_id [in bedrock.prelude.list_numbers]
insertZ_oob [in bedrock.prelude.list_numbers]
insertZ_nil [in bedrock.prelude.list_numbers]
insertZ_app_r [in bedrock.prelude.list_numbers]
insertZ_app_l [in bedrock.prelude.list_numbers]
insertZ_app_iff [in bedrock.prelude.list_numbers]
insertZ_cons_nz [in bedrock.prelude.list_numbers]
insertZ_cons_z [in bedrock.prelude.list_numbers]
insertZ_cons_iff [in bedrock.prelude.list_numbers]
insertZ_eq_insertN [in bedrock.prelude.list_numbers]
insert_seq [in bedrock.prelude.list_numbers]
introT [in bedrock.prelude.bool]
iso2lens_laws [in bedrock.prelude.lens]
isSomeP [in bedrock.prelude.option]
is_Some_proj_eq [in bedrock.prelude.option]
Is_true_eq [in bedrock.prelude.bool]
Is_true_is_true [in bedrock.prelude.bool]
L
lengthN_sliceZ_le [in bedrock.prelude.list_numbers]lengthN_sliceZ [in bedrock.prelude.list_numbers]
lengthN_rangeZ [in bedrock.prelude.list_numbers]
lengthN_insertZ [in bedrock.prelude.list_numbers]
lengthN_zip [in bedrock.prelude.list_numbers]
lengthN_insertN [in bedrock.prelude.list_numbers]
lengthN_replicateN [in bedrock.prelude.list_numbers]
lengthN_rotateN [in bedrock.prelude.list_numbers]
lengthN_takeN [in bedrock.prelude.list_numbers]
lengthN_dropN [in bedrock.prelude.list_numbers]
lengthN_map [in bedrock.prelude.list_numbers]
lengthN_app [in bedrock.prelude.list_numbers]
lengthN_one [in bedrock.prelude.list_numbers]
lengthN_cons [in bedrock.prelude.list_numbers]
lengthN_nil [in bedrock.prelude.list_numbers]
lengthN_fold [in bedrock.prelude.list_numbers]
lengthZ_sliceZ_iff [in bedrock.prelude.list_numbers]
lengthZ_eq_sub_iff [in bedrock.prelude.list_numbers]
length_takeN [in bedrock.prelude.list_numbers]
length_dropN [in bedrock.prelude.list_numbers]
length_lengthN [in bedrock.prelude.list_numbers]
ListNoDup_enum [in bedrock.prelude.finite]
list_ap_compose [in bedrock.prelude.list]
list_ap_singleton_r [in bedrock.prelude.list]
list_ap_singleton_l [in bedrock.prelude.list]
list_difference_remove [in bedrock.prelude.list]
list_remove_delete [in bedrock.prelude.list]
list_difference_delete [in bedrock.prelude.list]
list_singleton_eq_ext [in bedrock.prelude.list]
list_empty_eq_ext [in bedrock.prelude.list]
list_ne_length [in bedrock.prelude.list]
list_difference_singleton_not_in [in bedrock.prelude.list]
list_difference_app_r [in bedrock.prelude.list]
list_difference_cons_r [in bedrock.prelude.list]
list_difference_nil_r [in bedrock.prelude.list]
list_delete_elem_of_2 [in bedrock.prelude.list]
list_delete_elem_of_1 [in bedrock.prelude.list]
list_fmap_id' [in bedrock.prelude.list]
list_fmap_filter [in bedrock.prelude.list]
list_filter_insert [in bedrock.prelude.list]
list_filter_empty_iff [in bedrock.prelude.list]
list_alter_insert [in bedrock.prelude.list]
list_not_disjoint [in bedrock.prelude.list]
list_disjoint_alt [in bedrock.prelude.list]
list_equiv_symmetric_strong [in bedrock.prelude.list]
list_equiv_reflexive_strong [in bedrock.prelude.list]
list_alterN_insertN [in bedrock.prelude.list_numbers]
list_ne_lengthN [in bedrock.prelude.list_numbers]
list_lookupN_fmap [in bedrock.prelude.list_numbers]
list_alter_alterN [in bedrock.prelude.list_numbers]
list_alterN_alter [in bedrock.prelude.list_numbers]
list_insert_insertN [in bedrock.prelude.list_numbers]
list_insertN_insert [in bedrock.prelude.list_numbers]
list_lookup_lookupN [in bedrock.prelude.list_numbers]
list_lookupN_lookup [in bedrock.prelude.list_numbers]
list_In_enum [in bedrock.prelude.finite]
list_find_enum_total [in bedrock.prelude.finite]
lookupN_seqN [in bedrock.prelude.list_numbers]
lookupN_seqN_lt [in bedrock.prelude.list_numbers]
lookupN_seqN_ge [in bedrock.prelude.list_numbers]
lookupN_ge_None [in bedrock.prelude.list_numbers]
lookupN_explode [in bedrock.prelude.list_numbers]
lookupN_mid [in bedrock.prelude.list_numbers]
lookupN_any [in bedrock.prelude.list_numbers]
lookupN_rotateN [in bedrock.prelude.list_numbers]
lookupN_map [in bedrock.prelude.list_numbers]
lookupN_nth_error [in bedrock.prelude.list_numbers]
lookupN_insertN_neq [in bedrock.prelude.list_numbers]
lookupN_insertN_eq [in bedrock.prelude.list_numbers]
lookupN_app_r [in bedrock.prelude.list_numbers]
lookupN_app_l [in bedrock.prelude.list_numbers]
lookupN_tail [in bedrock.prelude.list_numbers]
lookupN_head [in bedrock.prelude.list_numbers]
lookupN_replicateN [in bedrock.prelude.list_numbers]
lookupN_bound [in bedrock.prelude.list_numbers]
lookupN_is_None [in bedrock.prelude.list_numbers]
lookupN_is_Some [in bedrock.prelude.list_numbers]
lookupN_takeN [in bedrock.prelude.list_numbers]
lookupN_dropN [in bedrock.prelude.list_numbers]
lookupN_cons_succ [in bedrock.prelude.list_numbers]
lookupN_cons_Nsucc [in bedrock.prelude.list_numbers]
lookupN_cons_zero [in bedrock.prelude.list_numbers]
lookupN_nil [in bedrock.prelude.list_numbers]
lookupN_fold [in bedrock.prelude.list_numbers]
lookupZ_singleton_Some [in bedrock.prelude.list_numbers]
lookupZ_insertZ_neq [in bedrock.prelude.list_numbers]
lookupZ_insertZ_eq [in bedrock.prelude.list_numbers]
lookupZ_insertZ [in bedrock.prelude.list_numbers]
lookupZ_cons [in bedrock.prelude.list_numbers]
lookupZ_app [in bedrock.prelude.list_numbers]
lookupZ_nil [in bedrock.prelude.list_numbers]
lookupZ_is_Some [in bedrock.prelude.list_numbers]
lookupZ_None_inv [in bedrock.prelude.list_numbers]
lookupZ_None [in bedrock.prelude.list_numbers]
lookupZ_Some_to_N [in bedrock.prelude.list_numbers]
lookupZ_Some_to_nat [in bedrock.prelude.list_numbers]
lookup_insert_iff [in bedrock.prelude.gmap]
M
mapM_fmap_Forall_Some_inv [in bedrock.prelude.list]map_fmap [in bedrock.prelude.list]
map_insertN [in bedrock.prelude.list_numbers]
map_Forall_fmap [in bedrock.prelude.fin_maps]
map_fmap_difference [in bedrock.prelude.fin_maps]
map_insert_difference [in bedrock.prelude.fin_maps]
map_difference_insert_ne [in bedrock.prelude.fin_maps]
map_difference_union_distr_disj_l [in bedrock.prelude.fin_maps]
map_difference_union_distr_l [in bedrock.prelude.fin_maps]
map_union_difference [in bedrock.prelude.fin_maps]
map_positive_r [in bedrock.prelude.fin_maps]
map_positive [in bedrock.prelude.fin_maps]
N
nat_fin_iter_le [in bedrock.prelude.list_numbers]nat_fin_iter_lt [in bedrock.prelude.list_numbers]
negP [in bedrock.prelude.bool]
NoDup_fmap_ap [in bedrock.prelude.list]
NoDup_ap [in bedrock.prelude.list]
NoDup_fmap_fun [in bedrock.prelude.list]
NoDup_zip_snd [in bedrock.prelude.list]
NoDup_zip_fst [in bedrock.prelude.list]
NoDup_zip_with_snd_inj [in bedrock.prelude.list]
NoDup_zip_with_snd_gen [in bedrock.prelude.list]
NoDup_zip_with_fst_inj [in bedrock.prelude.list]
NoDup_zip_with_fst_gen [in bedrock.prelude.list]
NoDup_not_in_delete [in bedrock.prelude.list]
NoDup_Permutation' [in bedrock.prelude.list]
NoDup_rangeZ [in bedrock.prelude.list_numbers]
NoDup_seqN [in bedrock.prelude.list_numbers]
NoDup_app_fmap_l [in bedrock.prelude.finite]
not_elem_of_list_lookup [in bedrock.prelude.list]
not_or [in bedrock.prelude.base]
not_pairwise_disjoint [in bedrock.prelude.fin_sets]
not_set_elem_of_bool_decide [in bedrock.prelude.fin_sets]
N_enumerate [in bedrock.prelude.list_numbers]
N_fin_iter_le [in bedrock.prelude.list_numbers]
N_fin_iter_lt [in bedrock.prelude.list_numbers]
N_to_Qp_mul [in bedrock.prelude.numbers]
N_to_Qp_add [in bedrock.prelude.numbers]
N_to_Qp_inj_lt [in bedrock.prelude.numbers]
N_to_Qp_inj_le [in bedrock.prelude.numbers]
N_to_Qp_inj_iff [in bedrock.prelude.numbers]
N_to_Qp_inj [in bedrock.prelude.numbers]
N_to_Qp_succ [in bedrock.prelude.numbers]
N_to_Qp_pos [in bedrock.prelude.numbers]
N_to_Qp_1 [in bedrock.prelude.numbers]
N_b2n_1 [in bedrock.prelude.numbers]
N_b2n_0 [in bedrock.prelude.numbers]
N_mul_divide_weaken_r [in bedrock.prelude.numbers]
N_mul_divide_weaken_l [in bedrock.prelude.numbers]
N_divide_add_cancel_l [in bedrock.prelude.numbers]
N_lxor_lt_pow2 [in bedrock.prelude.numbers]
N_lxor_lt_pow2_aux [in bedrock.prelude.numbers]
N_le_pred_lt [in bedrock.prelude.numbers]
N_lxor_mono_aux [in bedrock.prelude.numbers]
N_lor_mono_r [in bedrock.prelude.numbers]
N_land_mono_l [in bedrock.prelude.numbers]
N_land_mono_r [in bedrock.prelude.numbers]
N_setbit_bool_decide [in bedrock.prelude.numbers]
N_ones_spec [in bedrock.prelude.numbers]
N_leb_bool_decide [in bedrock.prelude.numbers]
N_eqb_bool_decide [in bedrock.prelude.numbers]
N_succ_lt_mono_inv [in bedrock.prelude.numbers]
N_of_nat_le_mono [in bedrock.prelude.numbers]
N_of_nat_lt_mono [in bedrock.prelude.numbers]
N_succ_pos_pred [in bedrock.prelude.numbers]
N_land_bit [in bedrock.prelude.numbers]
N_ext_iff [in bedrock.prelude.numbers]
N_ext [in bedrock.prelude.numbers]
N_minE [in bedrock.prelude.numbers]
N2Nat_inj_le [in bedrock.prelude.list_numbers]
N2Z_inj_divide [in bedrock.prelude.numbers]
N2Z_lnot [in bedrock.prelude.numbers]
N2Z_lnot_trim [in bedrock.prelude.numbers]
N2Z_lxor [in bedrock.prelude.numbers]
N2Z_shiftr [in bedrock.prelude.numbers]
N2Z_shiftl [in bedrock.prelude.numbers]
N2Z_lor [in bedrock.prelude.numbers]
N2Z_land [in bedrock.prelude.numbers]
O
option_list_nil [in bedrock.prelude.option]orP [in bedrock.prelude.bool]
OT_bs.lt_not_eq [in bedrock.prelude.bytestring_core]
OT_bs.lt_trans [in bedrock.prelude.bytestring_core]
OT_bs.eq_trans [in bedrock.prelude.bytestring_core]
OT_bs.eq_sym [in bedrock.prelude.bytestring_core]
OT_bs.eq_refl [in bedrock.prelude.bytestring_core]
OT_bs.lm [in bedrock.prelude.bytestring_core]
OT_byte.lt_not_eq [in bedrock.prelude.bytestring_core]
OT_byte.lt_trans [in bedrock.prelude.bytestring_core]
OT_byte.eq_trans [in bedrock.prelude.bytestring_core]
OT_byte.eq_sym [in bedrock.prelude.bytestring_core]
OT_byte.eq_refl [in bedrock.prelude.bytestring_core]
over_apply [in bedrock.prelude.lens]
over_apply_raw [in bedrock.prelude.lens]
P
page_align_ofs_eq [in bedrock.prelude.page]page_align_dn_offset_of [in bedrock.prelude.page]
page_align_up_below [in bedrock.prelude.page]
page_align_up_mod [in bedrock.prelude.page]
page_align_dn_mod [in bedrock.prelude.page]
page_align_dn_below [in bedrock.prelude.page]
PAGE_bits_size [in bedrock.prelude.page]
pairwise_disj_funs_fmap [in bedrock.prelude.list]
pairwise_disj_funs_cons [in bedrock.prelude.list]
pairwise_disj_funs_inj [in bedrock.prelude.list]
pairwise_disjoint_union [in bedrock.prelude.sets]
pairwise_disjoint_union_2 [in bedrock.prelude.sets]
pairwise_disjoint_union_1 [in bedrock.prelude.sets]
pairwise_disjoint_singleton [in bedrock.prelude.sets]
Pos_of_S [in bedrock.prelude.numbers]
pow2N_spec [in bedrock.prelude.numbers]
pred_nat_succ [in bedrock.prelude.numbers]
propset_singleton_equiv_unit [in bedrock.prelude.propset]
propset_singleton_equiv [in bedrock.prelude.propset]
Q
Qp.div_4 [in bedrock.prelude.numbers]Qp.half_half_quarter [in bedrock.prelude.numbers]
Qp.mul_2_2 [in bedrock.prelude.numbers]
Qp.mul_div [in bedrock.prelude.numbers]
Qp.quarter_half [in bedrock.prelude.numbers]
Qp.sub_all_Some [in bedrock.prelude.numbers]
Qp.sub_all_add_all [in bedrock.prelude.numbers]
Qp.third_two_thirds [in bedrock.prelude.numbers]
Qp.two_thirds_third [in bedrock.prelude.numbers]
R
rangeZ_snoc [in bedrock.prelude.list_numbers]rangeZ_app [in bedrock.prelude.list_numbers]
rangeZ_cons [in bedrock.prelude.list_numbers]
rangeZ_nil [in bedrock.prelude.list_numbers]
rangeZ_oob [in bedrock.prelude.list_numbers]
reachable_singleton [in bedrock.prelude.sts]
reachable_nil [in bedrock.prelude.sts]
refl_True [in bedrock.prelude.base]
repeatN_replicateN [in bedrock.prelude.list_numbers]
repeat_replicate [in bedrock.prelude.list]
repeat_replicateN [in bedrock.prelude.list_numbers]
replicateN_cons [in bedrock.prelude.list_numbers]
replicateN_succ' [in bedrock.prelude.list_numbers]
replicateN_succ [in bedrock.prelude.list_numbers]
replicateN_zero [in bedrock.prelude.list_numbers]
replicateN_plus [in bedrock.prelude.list_numbers]
replicateN_S [in bedrock.prelude.list_numbers]
replicateN_0 [in bedrock.prelude.list_numbers]
resizeN_takeN_le [in bedrock.prelude.list_numbers]
resizeN_le [in bedrock.prelude.list_numbers]
resizeN_takeN_eq [in bedrock.prelude.list_numbers]
resizeN_plusN [in bedrock.prelude.list_numbers]
resizeN_idemp [in bedrock.prelude.list_numbers]
resizeN_replicateN [in bedrock.prelude.list_numbers]
resizeN_nil [in bedrock.prelude.list_numbers]
resizeN_lengthN [in bedrock.prelude.list_numbers]
resizeN_0 [in bedrock.prelude.list_numbers]
resizeN_all [in bedrock.prelude.list_numbers]
resizeN_spec [in bedrock.prelude.list_numbers]
Roption_leq_eq_equiv [in bedrock.prelude.option]
Roption_leq_equiv [in bedrock.prelude.option]
Roption_leq_inv_l_Some [in bedrock.prelude.option]
Roption_leq_inv_l_Some_eq [in bedrock.prelude.option]
Roption_leq_None_inv [in bedrock.prelude.option]
Roption_leq_Some_l_inv [in bedrock.prelude.option]
Roption_leq_option_relation [in bedrock.prelude.option]
rotateN_replicateN [in bedrock.prelude.list_numbers]
rotateN_mid [in bedrock.prelude.list_numbers]
rotateN_index [in bedrock.prelude.list_numbers]
rotateN_succ [in bedrock.prelude.list_numbers]
rotateN_plus [in bedrock.prelude.list_numbers]
rotateN_modulo' [in bedrock.prelude.list_numbers]
rotateN_modulo [in bedrock.prelude.list_numbers]
rotateN_lengthN [in bedrock.prelude.list_numbers]
rotateN_one [in bedrock.prelude.list_numbers]
rotateN_zero [in bedrock.prelude.list_numbers]
rotateN_singleton [in bedrock.prelude.list_numbers]
rotateN_nil [in bedrock.prelude.list_numbers]
rotateN_iter [in bedrock.prelude.list_numbers]
rotateN_fold [in bedrock.prelude.list_numbers]
round_up_align_up [in bedrock.prelude.numbers]
round_down_align_dn [in bedrock.prelude.numbers]
rwP [in bedrock.prelude.bool]
S
same_property_partial_reflexive [in bedrock.prelude.option]same_property_reflexive_equiv [in bedrock.prelude.option]
same_property_intro [in bedrock.prelude.option]
same_property_iff [in bedrock.prelude.option]
seqN_sublist [in bedrock.prelude.list_numbers]
seqN_lengthN [in bedrock.prelude.list_numbers]
seqN_S_end_app' [in bedrock.prelude.list_numbers]
seqN_S_end_app [in bedrock.prelude.list_numbers]
seqN_S_start' [in bedrock.prelude.list_numbers]
seqN_S_start [in bedrock.prelude.list_numbers]
seqN_0 [in bedrock.prelude.list_numbers]
seqW_S_end_app' [in bedrock.prelude.wrap]
seqW_S_end_app [in bedrock.prelude.wrap]
set_concat_map_singleton_L [in bedrock.prelude.fin_sets]
set_concat_map_union_L [in bedrock.prelude.fin_sets]
set_concat_map_empty_L [in bedrock.prelude.fin_sets]
set_concat_map_singleton [in bedrock.prelude.fin_sets]
set_concat_map_union [in bedrock.prelude.fin_sets]
set_concat_map_empty [in bedrock.prelude.fin_sets]
set_map_empty_iff_L [in bedrock.prelude.fin_sets]
set_map_empty_iff [in bedrock.prelude.fin_sets]
set_map_ext [in bedrock.prelude.fin_sets]
set_map_disjoint_singleton_r [in bedrock.prelude.fin_sets]
set_map_disjoint_singleton_l [in bedrock.prelude.fin_sets]
set_map_disjoint [in bedrock.prelude.fin_sets]
set_map_compose_L [in bedrock.prelude.fin_sets]
set_map_compose [in bedrock.prelude.fin_sets]
set_map_id_L [in bedrock.prelude.fin_sets]
set_map_id [in bedrock.prelude.fin_sets]
set_elem_of_bool_decide [in bedrock.prelude.fin_sets]
set_not_disjoint [in bedrock.prelude.fin_sets]
set_not_Forall [in bedrock.prelude.fin_sets]
set_not_elem_of [in bedrock.prelude.fin_sets]
set_Forall_union_equiv [in bedrock.prelude.sets]
set_disjoint_not_Forall_2 [in bedrock.prelude.sets]
set_disjoint_not_Forall_1 [in bedrock.prelude.sets]
simple_finite_bits_aux.land_mask_idemp [in bedrock.prelude.finite]
simple_finite_bits_aux.mask_top_land_to_bits [in bedrock.prelude.finite]
simple_finite_bits_aux.all_bits_mask_top [in bedrock.prelude.finite]
simple_finite_bits_aux.N_testbit_mask_top_of_bit [in bedrock.prelude.finite]
simple_finite_bits_aux.to_bits_mod_pow2 [in bedrock.prelude.finite]
simple_finite_bits_aux.N_testbit_to_bits_high_false [in bedrock.prelude.finite]
simple_finite_bits_aux.N_testbit_to_bits' [in bedrock.prelude.finite]
simple_finite_bits_aux.N_testbit_all_bits [in bedrock.prelude.finite]
simple_finite_bits_aux.masked_opt_max [in bedrock.prelude.finite]
simple_finite_bits_aux.masked_max [in bedrock.prelude.finite]
simple_finite_bits_aux.of_bits_max [in bedrock.prelude.finite]
simple_finite_bitmask_type_mixin.to_list_max [in bedrock.prelude.finite]
size_set_rangeZ [in bedrock.prelude.fin_sets]
size_map_inj [in bedrock.prelude.fin_sets]
size_set_seq [in bedrock.prelude.fin_sets]
size_empty_iff_L [in bedrock.prelude.fin_sets]
sliceZ_insertN [in bedrock.prelude.list_numbers]
sliceZ_min_l [in bedrock.prelude.list_numbers]
sliceZ_max_r [in bedrock.prelude.list_numbers]
sliceZ_explode_insert [in bedrock.prelude.list_numbers]
sliceZ_explode [in bedrock.prelude.list_numbers]
sliceZ_app [in bedrock.prelude.list_numbers]
sliceZ_snoc_insertZ [in bedrock.prelude.list_numbers]
sliceZ_cons_insertZ [in bedrock.prelude.list_numbers]
sliceZ_snoc [in bedrock.prelude.list_numbers]
sliceZ_cons [in bedrock.prelude.list_numbers]
sliceZ_nil [in bedrock.prelude.list_numbers]
sliceZ_self [in bedrock.prelude.list_numbers]
sliceZ_crop [in bedrock.prelude.list_numbers]
sliceZ_crop_r [in bedrock.prelude.list_numbers]
sliceZ_crop_l [in bedrock.prelude.list_numbers]
some_Forall2_eq_iff [in bedrock.prelude.option]
some_Forall2_iff [in bedrock.prelude.option]
Sts.step_star_tau_comp [in bedrock.prelude.sts]
Sts.step_star_comp [in bedrock.prelude.sts]
subrelation_flip [in bedrock.prelude.base]
subset_of_enum [in bedrock.prelude.finite]
T
tail_length_eq [in bedrock.prelude.list]tail_length [in bedrock.prelude.list]
tail_drop [in bedrock.prelude.list_numbers]
takeN_sliceZ [in bedrock.prelude.list_numbers]
takeN_congr [in bedrock.prelude.list_numbers]
takeN_insertN_lt [in bedrock.prelude.list_numbers]
takeN_insertN_ge [in bedrock.prelude.list_numbers]
takeN_resizeN_le [in bedrock.prelude.list_numbers]
takeN_resizeN_plus [in bedrock.prelude.list_numbers]
takeN_resizeN [in bedrock.prelude.list_numbers]
takeN_resizeN_eq [in bedrock.prelude.list_numbers]
takeN_dropN_commute [in bedrock.prelude.list_numbers]
takeN_dropN [in bedrock.prelude.list_numbers]
takeN_takeN [in bedrock.prelude.list_numbers]
takeN_S_r [in bedrock.prelude.list_numbers]
takeN_S_r' [in bedrock.prelude.list_numbers]
takeN_cons_succ [in bedrock.prelude.list_numbers]
takeN_nil [in bedrock.prelude.list_numbers]
takeN_app [in bedrock.prelude.list_numbers]
takeN_singleton [in bedrock.prelude.list_numbers]
takeN_lengthN [in bedrock.prelude.list_numbers]
takeN_one [in bedrock.prelude.list_numbers]
takeN_zero [in bedrock.prelude.list_numbers]
takeN_replicateN_plus [in bedrock.prelude.list_numbers]
takeN_replicateN [in bedrock.prelude.list_numbers]
TCElemOf_iff [in bedrock.prelude.base]
TCLeq_nat [in bedrock.prelude.base]
TCLeq_N [in bedrock.prelude.base]
TCLeq_Z [in bedrock.prelude.base]
TCLeq_positive [in bedrock.prelude.base]
TCLeq_iff [in bedrock.prelude.base]
TCLt_nat [in bedrock.prelude.base]
TCLt_N [in bedrock.prelude.base]
TCLt_Z [in bedrock.prelude.base]
TCLt_positive [in bedrock.prelude.base]
TCLt_iff [in bedrock.prelude.base]
TEST.list_ap_interchange [in bedrock.prelude.list]
TEST.list_ap_morphism [in bedrock.prelude.list]
TEST.list_ap_compose [in bedrock.prelude.list]
TEST.list_ap_id [in bedrock.prelude.list]
Test.test1 [in bedrock.prelude.fin]
Test.test2 [in bedrock.prelude.fin]
to_nat_lengthN [in bedrock.prelude.list_numbers]
TO_UPSTREAM_TRANSPARENT.dsig_eq_pi [in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.f_equal_help [in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.bool_decide_pack [in bedrock.prelude.fin]
U
union_minus_r_L [in bedrock.prelude.sets]union_minus_r [in bedrock.prelude.sets]
union_minus_l_L [in bedrock.prelude.sets]
union_minus_l [in bedrock.prelude.sets]
unwrapN_succ_inj [in bedrock.prelude.wrap]
V
view_apply [in bedrock.prelude.lens]W
wrapN_add_0w_r [in bedrock.prelude.wrap]wrapN_add_0N_r [in bedrock.prelude.wrap]
wrapN_add_0w_l [in bedrock.prelude.wrap]
wrapN_add_0N_l [in bedrock.prelude.wrap]
wrapper.of_to_N [in bedrock.prelude.wrap]
wrapper.to_of_N [in bedrock.prelude.wrap]
Z
zip_lookup_Some [in bedrock.prelude.list]zip_lookupN_Some [in bedrock.prelude.list_numbers]
Z_rem_dev_eq [in bedrock.prelude.numbers]
Z_ones_nonneg [in bedrock.prelude.numbers]
Z_ones_pow2 [in bedrock.prelude.numbers]
Z_divide_gcd_iff' [in bedrock.prelude.numbers]
Z_b2z_1 [in bedrock.prelude.numbers]
Z_b2z_0 [in bedrock.prelude.numbers]
Z_pow2_half [in bedrock.prelude.numbers]
Z_mod_big [in bedrock.prelude.numbers]
Z_pow_max_distr_r [in bedrock.prelude.numbers]
Z_max_add_distr_r [in bedrock.prelude.numbers]
Z_max_add_distr_l [in bedrock.prelude.numbers]
Z_land_bit [in bedrock.prelude.numbers]
Z_ext_iff [in bedrock.prelude.numbers]
Z_ext [in bedrock.prelude.numbers]
Z_to_N_max_0 [in bedrock.prelude.numbers]
Z_of_N_Zto_N_eq_max [in bedrock.prelude.numbers]
Z_to_N_eq_0_iff [in bedrock.prelude.numbers]
Z_to_N_eq_0 [in bedrock.prelude.numbers]
Z2N_inj_divide [in bedrock.prelude.numbers]
Constructor Index
A
Alias.A [in bedrock.prelude.elpi.derive_test]Alias.B [in bedrock.prelude.elpi.derive_test]
B
BasicTests.A1 [in bedrock.prelude.elpi.derive_test]BasicTests.A2 [in bedrock.prelude.elpi.derive_test]
BasicTests.A2 [in bedrock.prelude.elpi.derive_test]
BasicTests.B1 [in bedrock.prelude.elpi.derive_test]
BasicTests.B2 [in bedrock.prelude.elpi.derive_test]
BasicTests.B2 [in bedrock.prelude.elpi.derive_test]
BasicTests.C1 [in bedrock.prelude.elpi.derive_test]
BasicTests.C2 [in bedrock.prelude.elpi.derive_test]
BasicTests.C2 [in bedrock.prelude.elpi.derive_test]
binder [in bedrock.prelude.named_binder]
BitsetTest.A [in bedrock.prelude.elpi.derive_test]
BitsetTest.B [in bedrock.prelude.elpi.derive_test]
BitsetTest.C [in bedrock.prelude.elpi.derive_test]
BitsetTest.D [in bedrock.prelude.elpi.derive_test]
BS.Buf.Append [in bedrock.prelude.bytestring_core]
BS.Buf.Byte [in bedrock.prelude.bytestring_core]
BS.Buf.Concat [in bedrock.prelude.bytestring_core]
BS.Buf.Empty [in bedrock.prelude.bytestring_core]
BS.Buf.String [in bedrock.prelude.bytestring_core]
BS.EmptyString [in bedrock.prelude.bytestring_core]
BS.String [in bedrock.prelude.bytestring_core]
C
compare [in bedrock.prelude.base]D
DerivingTest.A [in bedrock.prelude.elpi.derive_test]DerivingTest.B [in bedrock.prelude.elpi.derive_test]
DerivingTest.C [in bedrock.prelude.elpi.derive_test]
Deriving2Test.A [in bedrock.prelude.elpi.derive_test]
Deriving2Test.B [in bedrock.prelude.elpi.derive_test]
Deriving2Test.C [in bedrock.prelude.elpi.derive_test]
Deriving2Test.D [in bedrock.prelude.elpi.derive_test]
Deriving2Test.E [in bedrock.prelude.elpi.derive_test]
Deriving2Test.F [in bedrock.prelude.elpi.derive_test]
Deriving2Test.G [in bedrock.prelude.elpi.derive_test]
Deriving2Test.H [in bedrock.prelude.elpi.derive_test]
E
EdgeSig [in bedrock.prelude.interrupts]F
FiniteTest.A [in bedrock.prelude.elpi.derive_test]FiniteTest.B [in bedrock.prelude.elpi.derive_test]
FiniteTest.C [in bedrock.prelude.elpi.derive_test]
FiniteTest.D [in bedrock.prelude.elpi.derive_test]
FMapExtra.RAW.BSLeaf [in bedrock.prelude.avl]
FMapExtra.RAW.BSNode [in bedrock.prelude.avl]
FMapExtra.RAW.InLeft [in bedrock.prelude.avl]
FMapExtra.RAW.InRight [in bedrock.prelude.avl]
FMapExtra.RAW.InRoot [in bedrock.prelude.avl]
FMapExtra.RAW.Leaf [in bedrock.prelude.avl]
FMapExtra.RAW.Node [in bedrock.prelude.avl]
ForallT_cons [in bedrock.prelude.list]
ForallT_nil [in bedrock.prelude.list]
G
GuestInt [in bedrock.prelude.interrupts]H
HostInt [in bedrock.prelude.interrupts]I
IntEnabled [in bedrock.prelude.interrupts]InteropTests.A1 [in bedrock.prelude.elpi.derive_test]
InteropTests.A2 [in bedrock.prelude.elpi.derive_test]
InteropTests.B1 [in bedrock.prelude.elpi.derive_test]
InteropTests.B2 [in bedrock.prelude.elpi.derive_test]
InteropTests.C1 [in bedrock.prelude.elpi.derive_test]
InteropTests.C2 [in bedrock.prelude.elpi.derive_test]
intline_of [in bedrock.prelude.interrupts]
IntMasked [in bedrock.prelude.interrupts]
L
LevelSig [in bedrock.prelude.interrupts]N
N_non_zero [in bedrock.prelude.base]P
pairwise_disjoint [in bedrock.prelude.base]R
ReachableDone [in bedrock.prelude.sts]ReachableStep [in bedrock.prelude.sts]
Rleq_Some [in bedrock.prelude.option]
Rleq_None [in bedrock.prelude.option]
rPQ_false [in bedrock.prelude.bool]
rPQ_true [in bedrock.prelude.bool]
S
SimpleBitsetTest.A [in bedrock.prelude.elpi.derive_test]SimpleBitsetTest.B [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.C [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.D [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.A [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.A [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.B [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.B [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.C [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.C [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.D [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.D [in bedrock.prelude.elpi.derive_test]
Sts.HIDE [in bedrock.prelude.sts]
Sts.MAP_action [in bedrock.prelude.sts]
Sts.MAP_tau [in bedrock.prelude.sts]
Sts.PAR_right [in bedrock.prelude.sts]
Sts.PAR_left [in bedrock.prelude.sts]
Sts.PAR_comm [in bedrock.prelude.sts]
T
TCAndT_intro [in bedrock.prelude.tc_cond_type]TCForceEq_refl [in bedrock.prelude.named_binder]
TCLeq_lt [in bedrock.prelude.base]
TCLeq_eq [in bedrock.prelude.base]
TCLt_lt [in bedrock.prelude.base]
TCOrT_r [in bedrock.prelude.tc_cond_type]
TCOrT_l [in bedrock.prelude.tc_cond_type]
TriggerEdge [in bedrock.prelude.interrupts]
TriggerLevel [in bedrock.prelude.interrupts]
W
wrapN_notations.wrapN_add [in bedrock.prelude.wrap]Axiom Index
B
bitmask_type.to_bit [in bedrock.prelude.finite]E
eqdec_type.t [in bedrock.prelude.finite]ERROR.t [in bedrock.prelude.error]
F
finite_encoded_type.to_N [in bedrock.prelude.finite]FMapExtra.LEIBNIZ_EQ.eqL [in bedrock.prelude.avl]
FMapExtra.RAW.map [in bedrock.prelude.avl]
FMapExtra.RAW.mapi [in bedrock.prelude.avl]
FMapExtra.RAW.map_option [in bedrock.prelude.avl]
FMapExtra.RAW.map2 [in bedrock.prelude.avl]
FMapExtra.RAW.map2_opt [in bedrock.prelude.avl]
S
some_Forall2_Locked.unlock [in bedrock.prelude.option]some_Forall2_Locked.body [in bedrock.prelude.option]
Projection Index
A
attrs.read [in bedrock.prelude.page]attrs.sexec [in bedrock.prelude.page]
attrs.uexec [in bedrock.prelude.page]
attrs.write [in bedrock.prelude.page]
B
binder [in bedrock.prelude.named_binder]C
compare [in bedrock.prelude.base]compare_trans [in bedrock.prelude.base]
compare_antisym [in bedrock.prelude.base]
Compose.cancel_evt [in bedrock.prelude.sts]
Compose.cancel_evt_asym [in bedrock.prelude.sts]
Compose.external_event [in bedrock.prelude.sts]
Compose.inj_evt [in bedrock.prelude.sts]
Compose.name [in bedrock.prelude.sts]
Compose.name_finite [in bedrock.prelude.sts]
Compose.name_eq_dec [in bedrock.prelude.sts]
Compose.sts_name [in bedrock.prelude.sts]
F
FMapExtra.MAP.is_bst [in bedrock.prelude.avl]FMapExtra.MAP.this [in bedrock.prelude.avl]
FMapExtra.RAW.t_right [in bedrock.prelude.avl]
FMapExtra.RAW.t_opt [in bedrock.prelude.avl]
FMapExtra.RAW.t_left [in bedrock.prelude.avl]
I
intline_of [in bedrock.prelude.interrupts]int_status [in bedrock.prelude.interrupts]
int_owner [in bedrock.prelude.interrupts]
int_trigger [in bedrock.prelude.interrupts]
int_cpu [in bedrock.prelude.interrupts]
iso.f [in bedrock.prelude.lens]
iso.f_g [in bedrock.prelude.lens]
iso.g [in bedrock.prelude.lens]
iso.g_f [in bedrock.prelude.lens]
L
line [in bedrock.prelude.interrupts]N
name_inhabited [in bedrock.prelude.name]name_finite [in bedrock.prelude.name]
name_eq_dec [in bedrock.prelude.name]
N_non_zero [in bedrock.prelude.base]
P
pairwise_disjoint [in bedrock.prelude.base]pe_name_finite [in bedrock.prelude.name]
pe_name_eq_dec [in bedrock.prelude.name]
S
set_set [in bedrock.prelude.lens]set_view [in bedrock.prelude.lens]
Sts.Label [in bedrock.prelude.sts]
Sts._sts [in bedrock.prelude.sts]
Sts._step [in bedrock.prelude.sts]
Sts._init_state [in bedrock.prelude.sts]
Sts._state [in bedrock.prelude.sts]
T
to [in bedrock.prelude.interrupts]U
unwrapN [in bedrock.prelude.wrap]V
view_set [in bedrock.prelude.lens]view_over [in bedrock.prelude.lens]
W
wrapN_notations.wrapN_add [in bedrock.prelude.wrap]Inductive Index
A
Alias.T [in bedrock.prelude.elpi.derive_test]B
BasicTests.T1 [in bedrock.prelude.elpi.derive_test]BasicTests.T2 [in bedrock.prelude.elpi.derive_test]
BasicTests.T2 [in bedrock.prelude.elpi.derive_test]
Binder [in bedrock.prelude.named_binder]
BitsetTest.feature [in bedrock.prelude.elpi.derive_test]
BS.Buf.t [in bedrock.prelude.bytestring_core]
BS.t [in bedrock.prelude.bytestring_core]
C
Compare [in bedrock.prelude.base]D
DerivingTest._t [in bedrock.prelude.elpi.derive_test]Deriving2Test.t3 [in bedrock.prelude.elpi.derive_test]
Deriving2Test._t2 [in bedrock.prelude.elpi.derive_test]
Deriving2Test._t [in bedrock.prelude.elpi.derive_test]
F
FiniteTest.feature [in bedrock.prelude.elpi.derive_test]FMapExtra.RAW.bst [in bedrock.prelude.avl]
FMapExtra.RAW.In [in bedrock.prelude.avl]
FMapExtra.RAW.tree [in bedrock.prelude.avl]
ForallT [in bedrock.prelude.list]
I
InteropTests.T1 [in bedrock.prelude.elpi.derive_test]InteropTests.T2 [in bedrock.prelude.elpi.derive_test]
InterruptSignal [in bedrock.prelude.interrupts]
IntLines [in bedrock.prelude.interrupts]
IntOwner [in bedrock.prelude.interrupts]
IntStatus [in bedrock.prelude.interrupts]
IntTrigger [in bedrock.prelude.interrupts]
N
NNonZero [in bedrock.prelude.base]P
PairwiseDisjoint [in bedrock.prelude.base]R
reachable [in bedrock.prelude.sts]reflectPQ [in bedrock.prelude.bool]
Roption_leq [in bedrock.prelude.option]
S
SimpleBitsetTest.feature [in bedrock.prelude.elpi.derive_test]SimpleFiniteTest.feature [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature [in bedrock.prelude.elpi.derive_test]
Sts.Hide_step [in bedrock.prelude.sts]
Sts.Map_step [in bedrock.prelude.sts]
Sts.Par_step [in bedrock.prelude.sts]
T
TCAndT [in bedrock.prelude.tc_cond_type]TCForceEq [in bedrock.prelude.named_binder]
TCLeq [in bedrock.prelude.base]
TCLt [in bedrock.prelude.base]
TCOrT [in bedrock.prelude.tc_cond_type]
W
wrapN_notations.WrapNAdd [in bedrock.prelude.wrap]wrapper.Phant [in bedrock.prelude.wrap]
Section Index
A
add_opt [in bedrock.prelude.option]ap [in bedrock.prelude.list]
B
Binder [in bedrock.prelude.named_binder]C
char_parsec [in bedrock.prelude.parsec]compare [in bedrock.prelude.base]
compare [in bedrock.prelude.compare]
compare.derived [in bedrock.prelude.base]
Compose.Compose [in bedrock.prelude.sts]
Compose.Compose [in bedrock.prelude.sts]
countable [in bedrock.prelude.finite]
D
dep_fn_insert [in bedrock.prelude.functions]Deriving2Test.test [in bedrock.prelude.elpi.derive_test]
dom_map_seqZ [in bedrock.prelude.fin_map_dom]
E
enc_finite_N [in bedrock.prelude.finite]enc_finite [in bedrock.prelude.finite]
F
finite [in bedrock.prelude.finite]finite_bits_aux.BT_to_bit_inj [in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_bit_inj [in bedrock.prelude.finite]
finite_preimage_set.finite_preimage_set_leibniz [in bedrock.prelude.finite]
finite_preimage_set [in bedrock.prelude.finite]
finite_preimage.finite_preimage_inj [in bedrock.prelude.finite]
finite_preimage [in bedrock.prelude.finite]
finite_stdlib [in bedrock.prelude.finite]
finset [in bedrock.prelude.fin_sets]
finset.elements [in bedrock.prelude.fin_sets]
finset.elements.elements_leibniz [in bedrock.prelude.fin_sets]
fin_map_dom [in bedrock.prelude.fin_map_dom]
fin_prod.with_finite [in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_fg [in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_eq_dec [in bedrock.prelude.finite_prod]
fin_prod.internal.theory_with_type [in bedrock.prelude.finite_prod]
fin_prod.internal.with_eq_dec [in bedrock.prelude.finite_prod]
fin_prod.internal.with_fg [in bedrock.prelude.finite_prod]
fin_set [in bedrock.prelude.fin_sets]
fin_maps [in bedrock.prelude.fin_maps]
fin_fun_eq_dec [in bedrock.prelude.finite]
flip_app [in bedrock.prelude.base]
FMapExtra.MIXIN.canon [in bedrock.prelude.avl]
FMapExtra.MIXIN.map [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw [in bedrock.prelude.avl]
FMapExtra.RAW.bst [in bedrock.prelude.avl]
FMapExtra.RAW.ops [in bedrock.prelude.avl]
G
get_range_bitsN.get_range_bitsN_bounded_elim [in bedrock.prelude.bitsN]get_range_bitsN [in bedrock.prelude.bitsN]
gset_bind [in bedrock.prelude.gmap]
I
implb [in bedrock.prelude.bool]L
list [in bedrock.prelude.list]listN [in bedrock.prelude.list_numbers]
lists [in bedrock.prelude.list]
lists.zip_with [in bedrock.prelude.list]
listZ [in bedrock.prelude.list_numbers]
list_difference [in bedrock.prelude.list]
list.disjoint_dec [in bedrock.prelude.list]
lookup_insert [in bedrock.prelude.gmap]
M
monoid [in bedrock.prelude.lens]N
NoDup_fmap_ap [in bedrock.prelude.list]NoDup_ap [in bedrock.prelude.list]
O
on_props.on_props [in bedrock.prelude.option]Q
Qp.Qp_all [in bedrock.prelude.numbers]R
rangeZ [in bedrock.prelude.list_numbers]Roption_leq [in bedrock.prelude.option]
S
same_property.with_on_props [in bedrock.prelude.option]same_property [in bedrock.prelude.option]
semi_set [in bedrock.prelude.sets]
semi_set [in bedrock.prelude.sets]
seqN [in bedrock.prelude.list_numbers]
seqW [in bedrock.prelude.wrap]
set_rangeZ.dom_rangeZ [in bedrock.prelude.fin_sets]
set_rangeZ [in bedrock.prelude.fin_sets]
set_concat_map.set_concat_map_leibniz [in bedrock.prelude.fin_sets]
set_concat_map [in bedrock.prelude.fin_sets]
set_map [in bedrock.prelude.fin_sets]
set_map [in bedrock.prelude.fin_sets]
set_map_functorial.compose [in bedrock.prelude.fin_sets]
set_map_functorial [in bedrock.prelude.fin_sets]
set_seq [in bedrock.prelude.fin_sets]
sliceZ [in bedrock.prelude.list_numbers]
some_Forall2_eq [in bedrock.prelude.option]
some_Forall2 [in bedrock.prelude.option]
Sts.hide [in bedrock.prelude.sts]
Sts.map [in bedrock.prelude.sts]
Sts.par [in bedrock.prelude.sts]
T
top_set.leibniz [in bedrock.prelude.sets]top_set [in bedrock.prelude.sets]
TO_UPSTREAM_TRANSPARENT.dsig_transparent [in bedrock.prelude.fin]
type [in bedrock.prelude.wrap]
U
under_proper [in bedrock.prelude.under_rel_proper]W
with_N_to_Qp [in bedrock.prelude.numbers]with_Z [in bedrock.prelude.numbers]
_
_constr [in bedrock.prelude.lens]_apply_unfold [in bedrock.prelude.lens]
Instance Index
A
add_opt_inj [in bedrock.prelude.option]andb_right_absorb [in bedrock.prelude.bool]
andb_left_absorb [in bedrock.prelude.bool]
andb_right_id [in bedrock.prelude.bool]
andb_left_id [in bedrock.prelude.bool]
andb_assoc' [in bedrock.prelude.bool]
andb_comm' [in bedrock.prelude.bool]
applicative_fmap [in bedrock.prelude.base]
ap_Permutation [in bedrock.prelude.list]
attrs.t_countable [in bedrock.prelude.page]
attrs.t_inhabited [in bedrock.prelude.page]
attrs.t_eq_dec [in bedrock.prelude.page]
B
bool_compare [in bedrock.prelude.bool]Bool.le_preorder [in bedrock.prelude.bool]
Bool.le_pi [in bedrock.prelude.bool]
Bool.le_dec [in bedrock.prelude.bool]
bs_compare [in bedrock.prelude.bytestring_core]
bs_parse_string [in bedrock.prelude.parsec]
bs_next [in bedrock.prelude.parsec]
BS.append_right_id [in bedrock.prelude.bytestring_core]
BS.append_left_id [in bedrock.prelude.bytestring_core]
BS.Buf.empty [in bedrock.prelude.bytestring_core]
BS.Buf.monoid [in bedrock.prelude.bytestring_core]
BS.bytes_to_string_to_bytes [in bedrock.prelude.bytestring]
BS.parse_inj [in bedrock.prelude.bytestring_core]
BS.print_inj [in bedrock.prelude.bytestring_core]
bytestring_parse_surj [in bedrock.prelude.bytestring]
bytestring_print_surj [in bedrock.prelude.bytestring]
bytestring_parse_inj [in bedrock.prelude.bytestring]
bytestring_print_inj [in bedrock.prelude.bytestring]
bytestring_print_parse_cancel [in bedrock.prelude.bytestring]
bytestring_parse_print_cancel [in bedrock.prelude.bytestring]
bytestring_countable [in bedrock.prelude.bytestring]
bytestring_inhabited [in bedrock.prelude.bytestring]
bytestring_eq_dec [in bedrock.prelude.bytestring]
byte_of_N_surj [in bedrock.prelude.bytestring]
byte_to_N_inj [in bedrock.prelude.bytestring]
byte_countable [in bedrock.prelude.bytestring]
byte_eq_dec [in bedrock.prelude.bytestring]
byte_inhabited [in bedrock.prelude.bytestring]
byte_compare [in bedrock.prelude.bytestring_core]
C
cancel_Build_WrapN_unwrapN [in bedrock.prelude.wrap]cancel_unwrapN_Build_WrapN [in bedrock.prelude.wrap]
compare.eq_equiv [in bedrock.prelude.base]
compare.eq_dec [in bedrock.prelude.base]
compare.ge_dec [in bedrock.prelude.base]
compare.gt_dec [in bedrock.prelude.base]
compare.le_dec [in bedrock.prelude.base]
compare.lt_trans [in bedrock.prelude.base]
compare.lt_dec [in bedrock.prelude.base]
Compose.dual_sets_proper [in bedrock.prelude.sts]
E
elements_leibniz_inj [in bedrock.prelude.fin_sets]elements_perm [in bedrock.prelude.fin_sets]
elements_mono [in bedrock.prelude.fin_sets]
elements_inj [in bedrock.prelude.fin_sets]
encode_N_inj [in bedrock.prelude.finite]
eqdec_type.t_eq_dec [in bedrock.prelude.finite]
ERROR.exc [in bedrock.prelude.error]
F
FiniteTest.feature_to_N_inj [in bedrock.prelude.elpi.derive_test]finite_bits_aux.of_bits_surj [in bedrock.prelude.finite]
finite_bits_aux.to_bits_inj [in bedrock.prelude.finite]
finite_bits_aux.of_to_bits_cancel [in bedrock.prelude.finite]
finite_bits_aux.set_unfold_elem_of_to_list [in bedrock.prelude.finite]
finite_bits_aux.topset_t [in bedrock.prelude.finite]
finite_bits_aux.top_t [in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_testbit_to_bitmask_inj [in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_testbit_setbit_inj [in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_elem_of_to_list [in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_filter_0 [in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_filter [in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_testbit_land [in bedrock.prelude.finite]
finite_bitmask_type_mixin.set_unfold_testbit_lor [in bedrock.prelude.finite]
finite_type.t_finite [in bedrock.prelude.finite]
finite_preimage_set_params [in bedrock.prelude.finite]
finite_preimage_set_mono [in bedrock.prelude.finite]
finite_preimage_set_proper [in bedrock.prelude.finite]
fin_set_pairwise_disjoint_dec [in bedrock.prelude.fin_sets]
fin_fun_eq_pi [in bedrock.prelude.finite]
fin_fun_eq_dec [in bedrock.prelude.finite]
fin.to_N_inj [in bedrock.prelude.fin]
fin.t_finite [in bedrock.prelude.fin]
fin.t_pos_inhabited [in bedrock.prelude.fin]
fin.t_countable [in bedrock.prelude.fin]
fin.t_eq_dec [in bedrock.prelude.fin]
flip_app_assoc [in bedrock.prelude.base]
flip_app_right_id [in bedrock.prelude.base]
flip_app_left_id [in bedrock.prelude.base]
FMapExtra.MIXIN.key_eq_dec [in bedrock.prelude.avl]
FMapExtra.MIXIN.key_lt_dec [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_merge [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_map [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_partial_alter [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_singleton [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_mapfold [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_lookup [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_delete [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_insert [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_empty [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_omap [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_merge [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_map [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_singleton [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_mapfold [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_lookup [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_delete [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_insert [in bedrock.prelude.avl]
FMapExtra.MIXIN.raw_empty [in bedrock.prelude.avl]
fn_lookup_total [in bedrock.prelude.functions]
from_forall_named_binder [in bedrock.prelude.named_binder]
I
inj2_inj [in bedrock.prelude.base]IntAction_eq_dec [in bedrock.prelude.interrupts]
IntAction_inhabited [in bedrock.prelude.interrupts]
intcfg_valid_decision [in bedrock.prelude.interrupts]
InteropTests.manual_T2_finite [in bedrock.prelude.elpi.derive_test]
InteropTests.T1_eq_dec [in bedrock.prelude.elpi.derive_test]
InterruptSignal_eq_dec [in bedrock.prelude.interrupts]
InterruptSignal_inhabited [in bedrock.prelude.interrupts]
intline_elem_of_dec [in bedrock.prelude.interrupts]
into_exist_named_binder [in bedrock.prelude.named_binder]
int_types_match_decision [in bedrock.prelude.interrupts]
int_trigger_match_dec [in bedrock.prelude.interrupts]
int_cfg_decision [in bedrock.prelude.interrupts]
int_config_inhabited [in bedrock.prelude.interrupts]
int_status_decision [in bedrock.prelude.interrupts]
int_status_inhabited [in bedrock.prelude.interrupts]
int_owner_decision [in bedrock.prelude.interrupts]
int_owner_inhabited [in bedrock.prelude.interrupts]
int_trigger_decision [in bedrock.prelude.interrupts]
int_trigger_inhabited [in bedrock.prelude.interrupts]
L
lens_assoc [in bedrock.prelude.lens]lens_right_id [in bedrock.prelude.lens]
lens_left_id [in bedrock.prelude.lens]
lens_union [in bedrock.prelude.lens]
lens_unit [in bedrock.prelude.lens]
listset_nodup_elem_of_dec [in bedrock.prelude.listset_nodup]
list_disjoint_dec [in bedrock.prelude.list]
list_bind_perm [in bedrock.prelude.list]
list_bind_mono [in bedrock.prelude.list]
list_insertZ [in bedrock.prelude.list_numbers]
list_lookupZ [in bedrock.prelude.list_numbers]
list_alterN [in bedrock.prelude.list_numbers]
list_insertN [in bedrock.prelude.list_numbers]
list_lookupN [in bedrock.prelude.list_numbers]
list_to_set_mono [in bedrock.prelude.fin_sets]
list_to_set_elements_cancel_L [in bedrock.prelude.fin_sets]
list_to_set_elements_cancel [in bedrock.prelude.fin_sets]
M
map_inj [in bedrock.prelude.list]MkWrapN_inj [in bedrock.prelude.wrap]
monad_ap [in bedrock.prelude.base]
N
Nat_shiftr_right_id [in bedrock.prelude.numbers]Nat_shiftr_left_absorb [in bedrock.prelude.numbers]
Nat_shiftl_right_id [in bedrock.prelude.numbers]
Nat_shiftl_left_absorb [in bedrock.prelude.numbers]
Nat_lor_right_id [in bedrock.prelude.numbers]
Nat_lor_left_id [in bedrock.prelude.numbers]
Nat_lor_assoc [in bedrock.prelude.numbers]
Nat_lor_comm [in bedrock.prelude.numbers]
Nat_land_right_absorb [in bedrock.prelude.numbers]
Nat_land_left_absorb [in bedrock.prelude.numbers]
Nat_land_assoc [in bedrock.prelude.numbers]
Nat_land_comm [in bedrock.prelude.numbers]
Nat_max_assoc [in bedrock.prelude.numbers]
Nat_max_comm [in bedrock.prelude.numbers]
Nat_min_assoc [in bedrock.prelude.numbers]
Nat_min_comm [in bedrock.prelude.numbers]
Nat_trychotomyT [in bedrock.prelude.numbers]
Nat_mul_right_absorb [in bedrock.prelude.numbers]
Nat_mul_left_absorb [in bedrock.prelude.numbers]
Nat_mul_right_id [in bedrock.prelude.numbers]
Nat_mul_left_id [in bedrock.prelude.numbers]
Nat_mul_comm [in bedrock.prelude.numbers]
Nat_mul_assoc [in bedrock.prelude.numbers]
Nat_add_right_id [in bedrock.prelude.numbers]
Nat_add_left_id [in bedrock.prelude.numbers]
Nat_add_comm [in bedrock.prelude.numbers]
Nat_add_assoc [in bedrock.prelude.numbers]
nat_compare [in bedrock.prelude.numbers]
Nat2N_id_cancel [in bedrock.prelude.numbers]
Nat2Z_id_cancel [in bedrock.prelude.numbers]
N_non_empty [in bedrock.prelude.base]
N_b2n_inj [in bedrock.prelude.numbers]
N_divide_dec [in bedrock.prelude.numbers]
N_succ_inj [in bedrock.prelude.numbers]
N_shiftr_right_id [in bedrock.prelude.numbers]
N_shiftr_left_absorb [in bedrock.prelude.numbers]
N_shiftl_right_id [in bedrock.prelude.numbers]
N_shiftl_left_absorb [in bedrock.prelude.numbers]
N_lor_right_id [in bedrock.prelude.numbers]
N_lor_left_id [in bedrock.prelude.numbers]
N_lor_assoc [in bedrock.prelude.numbers]
N_lor_comm [in bedrock.prelude.numbers]
N_land_right_absorb [in bedrock.prelude.numbers]
N_land_left_absorb [in bedrock.prelude.numbers]
N_land_assoc [in bedrock.prelude.numbers]
N_land_comm [in bedrock.prelude.numbers]
N_max_assoc [in bedrock.prelude.numbers]
N_max_comm [in bedrock.prelude.numbers]
N_min_assoc [in bedrock.prelude.numbers]
N_min_comm [in bedrock.prelude.numbers]
N_trychotomyT [in bedrock.prelude.numbers]
N_mul_right_absorb [in bedrock.prelude.numbers]
N_mul_left_absorb [in bedrock.prelude.numbers]
N_mul_right_id [in bedrock.prelude.numbers]
N_mul_left_id [in bedrock.prelude.numbers]
N_mul_comm [in bedrock.prelude.numbers]
N_mul_assoc [in bedrock.prelude.numbers]
N_add_right_id [in bedrock.prelude.numbers]
N_add_left_id [in bedrock.prelude.numbers]
N_add_comm [in bedrock.prelude.numbers]
N_add_assoc [in bedrock.prelude.numbers]
N_comparison [in bedrock.prelude.numbers]
N_compare [in bedrock.prelude.numbers]
N2Nat_id_cancel [in bedrock.prelude.numbers]
N2Z_id_cancel [in bedrock.prelude.numbers]
O
on_props.on_total_order [in bedrock.prelude.option]on_props.on_partial_order [in bedrock.prelude.option]
on_props.on_trichotomyT [in bedrock.prelude.option]
on_props.on_trichotomy [in bedrock.prelude.option]
on_props.on_antisymm_eq_inj [in bedrock.prelude.option]
on_props.on_antisymm [in bedrock.prelude.option]
on_props.on_strict_order [in bedrock.prelude.option]
on_props.on_per [in bedrock.prelude.option]
on_props.on_preorder [in bedrock.prelude.option]
on_props.on_equivalence [in bedrock.prelude.option]
on_props.on_transitive [in bedrock.prelude.option]
on_props.on_asymmetric [in bedrock.prelude.option]
on_props.on_symmetric [in bedrock.prelude.option]
on_props.on_irreflexive [in bedrock.prelude.option]
on_props.on_reflexive [in bedrock.prelude.option]
on_props.on_decidable [in bedrock.prelude.option]
option_Forall2_decision [in bedrock.prelude.option]
orb_right_absorb [in bedrock.prelude.bool]
orb_left_absorb [in bedrock.prelude.bool]
orb_right_id [in bedrock.prelude.bool]
orb_left_id [in bedrock.prelude.bool]
orb_assoc' [in bedrock.prelude.bool]
orb_comm' [in bedrock.prelude.bool]
P
positive_comparison [in bedrock.prelude.numbers]positive_compare [in bedrock.prelude.numbers]
preorder_proper [in bedrock.prelude.base]
Q
Qc_compare [in bedrock.prelude.numbers]Qp.div_right_id [in bedrock.prelude.numbers]
Qp.mul_right_id [in bedrock.prelude.numbers]
Qp.mul_left_id [in bedrock.prelude.numbers]
Q_compare [in bedrock.prelude.numbers]
R
reflexive_proper [in bedrock.prelude.base]S
same_property_per [in bedrock.prelude.option]same_property_decision [in bedrock.prelude.option]
sc_reflexive [in bedrock.prelude.relations]
set_unfold_list_fmap_ap [in bedrock.prelude.list]
set_unfold_list_ap [in bedrock.prelude.list]
set_unfold_list_omap [in bedrock.prelude.list]
set_unfold_list_mjoin [in bedrock.prelude.list]
set_unfold_list_ret [in bedrock.prelude.list]
set_unfold_in [in bedrock.prelude.list]
set_unfold_list_intersection_with [in bedrock.prelude.list]
set_unfold_list_union [in bedrock.prelude.list]
set_unfold_list_intersection [in bedrock.prelude.list]
set_unfold_list_difference [in bedrock.prelude.list]
set_unfold_list_filter [in bedrock.prelude.list]
set_unfold_list_bind [in bedrock.prelude.list]
set_unfold_elem_of_seqN [in bedrock.prelude.list_numbers]
set_unfold_elem_of_seq [in bedrock.prelude.list_numbers]
set_concat_map_params [in bedrock.prelude.fin_sets]
set_unfold_set_concat_map [in bedrock.prelude.fin_sets]
set_concat_map_mono [in bedrock.prelude.fin_sets]
set_concat_map_perm_proper [in bedrock.prelude.fin_sets]
set_map_cancel [in bedrock.prelude.fin_sets]
set_map_inj_L [in bedrock.prelude.fin_sets]
set_map_inj [in bedrock.prelude.fin_sets]
set_unfold_gset_bind [in bedrock.prelude.gmap]
set_pairwise_disjoint_symmetric [in bedrock.prelude.sets]
set_pairwise_disjoint [in bedrock.prelude.sets]
set_unfold_bool_decide [in bedrock.prelude.bool]
set_unfold_orb [in bedrock.prelude.bool]
set_unfold_andb [in bedrock.prelude.bool]
set_unfold_negb [in bedrock.prelude.bool]
set_unfold_decode_N_None [in bedrock.prelude.finite]
set_unfold_decode_N_Some [in bedrock.prelude.finite]
set_unfold_finite_preimage_set [in bedrock.prelude.finite]
set_unfold_finite_inverse_inj_Some [in bedrock.prelude.finite]
set_unfold_finite_inverse_None [in bedrock.prelude.finite]
set_unfold_finite_preimage [in bedrock.prelude.finite]
set_unfold_elem_of_enum [in bedrock.prelude.finite]
some_Forall2_decision [in bedrock.prelude.option]
some_Forall2_per [in bedrock.prelude.option]
some_Forall2_transitive [in bedrock.prelude.option]
some_Forall2_symmetric [in bedrock.prelude.option]
T
tc_symmetric [in bedrock.prelude.relations]tc_reflexive [in bedrock.prelude.relations]
top_set_intersection_top_r_L [in bedrock.prelude.sets]
top_set_intersection_top_l_L [in bedrock.prelude.sets]
top_set_intersection_top_r [in bedrock.prelude.sets]
top_set_intersection_top_l [in bedrock.prelude.sets]
TO_UPSTREAM_TRANSPARENT.countable_dsig [in bedrock.prelude.fin]
TO_UPSTREAM_TRANSPARENT.dsig_eq_dec [in bedrock.prelude.fin]
transitive_proper [in bedrock.prelude.base]
U
under_proper [in bedrock.prelude.under_rel_proper]under_flip_mono [in bedrock.prelude.under_rel_proper]
under_mono [in bedrock.prelude.under_rel_proper]
unwrapN_inj [in bedrock.prelude.wrap]
W
wrapN_notations.wrapNwrapN_add [in bedrock.prelude.wrap]wrapN_notations.NwrapN_add [in bedrock.prelude.wrap]
wrapN_notations.wrapNN_add [in bedrock.prelude.wrap]
wrapN_inhabited [in bedrock.prelude.wrap]
wrapN_countable [in bedrock.prelude.wrap]
wrapN_eq_decision [in bedrock.prelude.wrap]
Z
Zabs2Nat_id_cancel [in bedrock.prelude.numbers]Zabs2N_id_cancel [in bedrock.prelude.numbers]
Z_divide_dec [in bedrock.prelude.numbers]
Z_b2z_inj [in bedrock.prelude.numbers]
Z_pred_inj [in bedrock.prelude.numbers]
Z_succ_inj [in bedrock.prelude.numbers]
Z_shiftr_right_id [in bedrock.prelude.numbers]
Z_shiftr_left_absorb [in bedrock.prelude.numbers]
Z_shiftl_right_id [in bedrock.prelude.numbers]
Z_shiftl_left_absorb [in bedrock.prelude.numbers]
Z_lor_right_id [in bedrock.prelude.numbers]
Z_lor_left_id [in bedrock.prelude.numbers]
Z_lor_assoc [in bedrock.prelude.numbers]
Z_lor_comm [in bedrock.prelude.numbers]
Z_land_right_absorb [in bedrock.prelude.numbers]
Z_land_left_absorb [in bedrock.prelude.numbers]
Z_land_assoc [in bedrock.prelude.numbers]
Z_land_comm [in bedrock.prelude.numbers]
Z_max_assoc [in bedrock.prelude.numbers]
Z_max_comm [in bedrock.prelude.numbers]
Z_min_assoc [in bedrock.prelude.numbers]
Z_min_comm [in bedrock.prelude.numbers]
Z_trychotomyT [in bedrock.prelude.numbers]
Z_mul_right_absorb [in bedrock.prelude.numbers]
Z_mul_left_absorb [in bedrock.prelude.numbers]
Z_mul_right_id [in bedrock.prelude.numbers]
Z_mul_left_id [in bedrock.prelude.numbers]
Z_mul_comm [in bedrock.prelude.numbers]
Z_mul_assoc [in bedrock.prelude.numbers]
Z_add_right_id [in bedrock.prelude.numbers]
Z_add_left_id [in bedrock.prelude.numbers]
Z_add_comm [in bedrock.prelude.numbers]
Z_add_assoc [in bedrock.prelude.numbers]
Z_comparison [in bedrock.prelude.numbers]
Z_compare [in bedrock.prelude.numbers]
Abbreviation Index
A
alterN [in bedrock.prelude.list_numbers]ap [in bedrock.prelude.list]
attrs.user [in bedrock.prelude.page]
B
Beta [in bedrock.prelude.base]BS.Byte [in bedrock.prelude.bytestring_core]
BS.Bytestring_notations.bs [in bedrock.prelude.bytestring_core]
BS.sepBy [in bedrock.prelude.bytestring]
BS.to_N_inj [in bedrock.prelude.bytestring_core]
build [in bedrock.prelude.avl]
Build_WrapN [in bedrock.prelude.wrap]
C
Cbn [in bedrock.prelude.base]check_canon_ok [in bedrock.prelude.avl]
check_canon_lem [in bedrock.prelude.avl]
check_canon [in bedrock.prelude.avl]
cpuT [in bedrock.prelude.hw_types]
D
dep_fn_insert_ne [in bedrock.prelude.functions]dep_fn_insert_eq [in bedrock.prelude.functions]
Disjoint [in bedrock.prelude.list]
E
Evaluate [in bedrock.prelude.base]F
find_any_ok [in bedrock.prelude.avl]find_any [in bedrock.prelude.avl]
finite_bitmask_type_mixin.setbit_alt [in bedrock.prelude.finite]
finite_preimage_gset [in bedrock.prelude.finite]
fin.lit [in bedrock.prelude.fin]
fin.of_idx_fin [in bedrock.prelude.fin]
fin.to_idx_fin [in bedrock.prelude.fin]
fin.weaken [in bedrock.prelude.fin]
FMapExtra.MIXIN_LEIBNIZ.K [in bedrock.prelude.avl]
FMapExtra.MIXIN.K [in bedrock.prelude.avl]
FMapExtra.MIXIN.M [in bedrock.prelude.avl]
FMapExtra.MIXIN.M [in bedrock.prelude.avl]
FMapExtra.RAW.key [in bedrock.prelude.avl]
FMapExtra.RAW.t [in bedrock.prelude.avl]
FMapExtra.RAW.t [in bedrock.prelude.avl]
FMapExtra.RAW.t [in bedrock.prelude.avl]
from_raw [in bedrock.prelude.avl]
from_raw_or [in bedrock.prelude.avl]
G
gset_concat_map [in bedrock.prelude.gmap]gset_map [in bedrock.prelude.gmap]
H
Hnf [in bedrock.prelude.base]I
IMR_omap [in bedrock.prelude.avl]IMR_delete [in bedrock.prelude.avl]
IMR_singleton [in bedrock.prelude.avl]
IMR_mapfold [in bedrock.prelude.avl]
IMR_merge [in bedrock.prelude.avl]
IMR_map [in bedrock.prelude.avl]
IMR_insert [in bedrock.prelude.avl]
IMR_empty [in bedrock.prelude.avl]
IMR_lookup [in bedrock.prelude.avl]
IM_partial_alter [in bedrock.prelude.avl]
IM_delete [in bedrock.prelude.avl]
IM_singleton [in bedrock.prelude.avl]
IM_mapfold [in bedrock.prelude.avl]
IM_merge [in bedrock.prelude.avl]
IM_map [in bedrock.prelude.avl]
IM_insert [in bedrock.prelude.avl]
IM_empty [in bedrock.prelude.avl]
IM_lookup [in bedrock.prelude.avl]
insertN [in bedrock.prelude.list_numbers]
L
lengthZ [in bedrock.prelude.list_numbers]list_ap_cons_r_p [in bedrock.prelude.list]
list_ap_cons_l [in bedrock.prelude.list]
list_ap_nil_r [in bedrock.prelude.list]
list_ap_nil_l [in bedrock.prelude.list]
list_difference_id [in bedrock.prelude.list]
lookupN [in bedrock.prelude.list_numbers]
LTS [in bedrock.prelude.sts]
lts_init_state [in bedrock.prelude.sts]
lts_step [in bedrock.prelude.sts]
lts_state [in bedrock.prelude.sts]
M
M [in bedrock.prelude.parsec]map_to_list_elements [in bedrock.prelude.avl]
map_canon [in bedrock.prelude.avl]
O
on [in bedrock.prelude.option]opteT [in bedrock.prelude.page]
P
page_aligned [in bedrock.prelude.page]Pos.compare_cont_Lt_Eq_discr [in bedrock.prelude.numbers]
Pos.compare_cont_Gt_Eq_discr [in bedrock.prelude.numbers]
pteT [in bedrock.prelude.page]
Q
Qp_div_right_id [in bedrock.prelude.numbers]Qp_mul_right_id [in bedrock.prelude.numbers]
Qp_mul_left_id [in bedrock.prelude.numbers]
R
Reduce [in bedrock.prelude.base]Refine [in bedrock.prelude.base]
repeatN [in bedrock.prelude.list_numbers]
replicateZ [in bedrock.prelude.list_numbers]
S
sepBy [in bedrock.prelude.bytestring]set_map [in bedrock.prelude.fin_sets]
set_map [in bedrock.prelude.fin_sets]
succ_wrapper.seqW [in bedrock.prelude.wrap]
succ_wrapper.succ [in bedrock.prelude.wrap]
T
types.Build_size_bytes [in bedrock.prelude.hw_types]types.Build_mmio_idx [in bedrock.prelude.hw_types]
types.Build_cpu [in bedrock.prelude.hw_types]
types.Build_time [in bedrock.prelude.hw_types]
types.Build_int_line [in bedrock.prelude.hw_types]
types.cpu [in bedrock.prelude.hw_types]
types.get_size_bytes [in bedrock.prelude.hw_types]
types.get_mmio_idx [in bedrock.prelude.hw_types]
types.get_cpu [in bedrock.prelude.hw_types]
types.get_time [in bedrock.prelude.hw_types]
types.get_int_line [in bedrock.prelude.hw_types]
types.int_line [in bedrock.prelude.hw_types]
types.mmio_idx [in bedrock.prelude.hw_types]
types.size_bytes [in bedrock.prelude.hw_types]
types.time [in bedrock.prelude.hw_types]
U
Unfold [in bedrock.prelude.base]Definition Index
A
add_opt [in bedrock.prelude.option]Alias.Countable.OnAliasDirect.t1_countable [in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasDirect.t1_eq_dec [in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasIndirect.t2_countable [in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnAliasIndirect.t2_eq_dec [in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnVariant.T_countable [in bedrock.prelude.elpi.derive_test]
Alias.Countable.OnVariant.T_eq_dec [in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnAliasIndirect.t2_eq_dec [in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnAliasDirect.t1_eq_dec [in bedrock.prelude.elpi.derive_test]
Alias.Eq_Dec.OnVariant.T_eq_dec [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect.t1_finite [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect.t1_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect.t1_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasDirect.t1_eq_dec [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect.t2_finite [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect.t2_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect.t2_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnAliasIndirect.t2_eq_dec [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant.T_finite [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant.T_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant.T_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
Alias.Finite.OnVariant.T_eq_dec [in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnAliasDirect.t1_inhabited [in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnAliasIndirect.t2_inhabited [in bedrock.prelude.elpi.derive_test]
Alias.Inhabited.OnVariant.T_inhabited [in bedrock.prelude.elpi.derive_test]
Alias.t1 [in bedrock.prelude.elpi.derive_test]
Alias.t2 [in bedrock.prelude.elpi.derive_test]
align_up [in bedrock.prelude.numbers]
align_dn [in bedrock.prelude.numbers]
attrs.is_rwsx [in bedrock.prelude.page]
attrs.is_rwux [in bedrock.prelude.page]
attrs.is_rw [in bedrock.prelude.page]
attrs.is_r [in bedrock.prelude.page]
attrs.masked [in bedrock.prelude.page]
attrs.masked_opt [in bedrock.prelude.page]
attrs.none [in bedrock.prelude.page]
attrs.nonnull [in bedrock.prelude.page]
attrs.opteT [in bedrock.prelude.page]
attrs.opte_mask [in bedrock.prelude.page]
attrs.pteT [in bedrock.prelude.page]
attrs.R [in bedrock.prelude.page]
attrs.RW [in bedrock.prelude.page]
attrs.RWX [in bedrock.prelude.page]
attrs.W [in bedrock.prelude.page]
B
BasicTests.T1_finite [in bedrock.prelude.elpi.derive_test]BasicTests.T1_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
BasicTests.T1_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
BasicTests.T1_countable [in bedrock.prelude.elpi.derive_test]
BasicTests.T1_inhabited [in bedrock.prelude.elpi.derive_test]
BasicTests.T1_eq_dec [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_countable [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_inhabited [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_eq_dec [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
BasicTests.T2_eq_dec [in bedrock.prelude.elpi.derive_test]
bindM2 [in bedrock.prelude.base]
bitmask_type_simple_mixin.of_bit [in bedrock.prelude.finite]
bitmask_type_simple_mixin.to_bit [in bedrock.prelude.finite]
BitsetTest.feature_finite [in bedrock.prelude.elpi.derive_test]
BitsetTest.feature_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
BitsetTest.feature_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
BitsetTest.feature_eq_dec [in bedrock.prelude.elpi.derive_test]
BitsetTest.feature.t [in bedrock.prelude.elpi.derive_test]
BitsetTest.feature.to_bit [in bedrock.prelude.elpi.derive_test]
BitsetTest.feature.t_finite [in bedrock.prelude.elpi.derive_test]
BitsetTest.feature.t_eq_dec [in bedrock.prelude.elpi.derive_test]
BitsetTest.Unnamed_thm1 [in bedrock.prelude.elpi.derive_test]
BitsetTest.Unnamed_thm0 [in bedrock.prelude.elpi.derive_test]
BitsetTest.Unnamed_thm [in bedrock.prelude.elpi.derive_test]
Bool.leb [in bedrock.prelude.bool]
bs_cmp [in bedrock.prelude.bytestring_core]
BS.append [in bedrock.prelude.bytestring_core]
BS.append_tailrec [in bedrock.prelude.bytestring_core]
BS.Buf.concat_aux [in bedrock.prelude.bytestring_core]
BS.Buf.contents [in bedrock.prelude.bytestring_core]
BS.Buf.contents_aux [in bedrock.prelude.bytestring_core]
BS.Buf.t_sind [in bedrock.prelude.bytestring_core]
BS.Buf.t_rec [in bedrock.prelude.bytestring_core]
BS.Buf.t_ind [in bedrock.prelude.bytestring_core]
BS.Buf.t_rect [in bedrock.prelude.bytestring_core]
BS.bytes_to_string [in bedrock.prelude.bytestring]
BS.concat [in bedrock.prelude.bytestring_core]
BS.concat_aux [in bedrock.prelude.bytestring_core]
BS.contains [in bedrock.prelude.bytestring_core]
BS.decimal_digit [in bedrock.prelude.bytestring]
BS.drop [in bedrock.prelude.bytestring]
BS.eqb [in bedrock.prelude.bytestring_core]
BS.eq_dec [in bedrock.prelude.bytestring_core]
BS.index [in bedrock.prelude.bytestring_core]
BS.last [in bedrock.prelude.bytestring]
BS.length [in bedrock.prelude.bytestring_core]
BS.of_N_decimal [in bedrock.prelude.bytestring]
BS.of_string [in bedrock.prelude.bytestring]
BS.parse [in bedrock.prelude.bytestring_core]
BS.pp_N_aux [in bedrock.prelude.bytestring]
BS.prefix [in bedrock.prelude.bytestring_core]
BS.print [in bedrock.prelude.bytestring_core]
BS.rev [in bedrock.prelude.bytestring_core]
BS.rev_append [in bedrock.prelude.bytestring_core]
BS.split_at [in bedrock.prelude.bytestring]
BS.split_at_loop [in bedrock.prelude.bytestring]
BS.string_to_bytes [in bedrock.prelude.bytestring]
BS.substring [in bedrock.prelude.bytestring_core]
BS.take [in bedrock.prelude.bytestring]
BS.to_string [in bedrock.prelude.bytestring]
BS.t_sind [in bedrock.prelude.bytestring_core]
BS.t_rec [in bedrock.prelude.bytestring_core]
BS.t_ind [in bedrock.prelude.bytestring_core]
BS.t_rect [in bedrock.prelude.bytestring_core]
byte_cmp [in bedrock.prelude.bytestring_core]
byte_print [in bedrock.prelude.bytestring_core]
byte_parse [in bedrock.prelude.bytestring_core]
C
card_N [in bedrock.prelude.finite]compare_lex [in bedrock.prelude.compare]
compare_tag [in bedrock.prelude.compare]
compare_ctor [in bedrock.prelude.compare]
compare.eq [in bedrock.prelude.base]
compare.ge [in bedrock.prelude.base]
compare.gt [in bedrock.prelude.base]
compare.le [in bedrock.prelude.base]
compare.lt [in bedrock.prelude.base]
Compose.compose_lts [in bedrock.prelude.sts]
Compose.dual_sets [in bedrock.prelude.sts]
Compose.eq_except [in bedrock.prelude.sts]
Compose.init_state [in bedrock.prelude.sts]
Compose.make [in bedrock.prelude.sts]
Compose.State [in bedrock.prelude.sts]
Compose._fam_sts [in bedrock.prelude.sts]
cpu.count [in bedrock.prelude.hw_types]
cpu.max [in bedrock.prelude.hw_types]
D
decode_from_encode [in bedrock.prelude.elpi.derive.countable]decode_N [in bedrock.prelude.finite]
deps [in bedrock.prelude.dummy]
dep_fn_insert [in bedrock.prelude.functions]
DerivingTest.t [in bedrock.prelude.elpi.derive_test]
DerivingTest.t_countable [in bedrock.prelude.elpi.derive_test]
DerivingTest.t_eq_dec [in bedrock.prelude.elpi.derive_test]
DerivingTest.Unnamed_thm1 [in bedrock.prelude.elpi.derive_test]
DerivingTest.Unnamed_thm0 [in bedrock.prelude.elpi.derive_test]
DerivingTest.Unnamed_thm [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_finite2 [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_finite [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t_inhabited [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2 [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_finite [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_inhabited [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t2_eq_dec [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_finite [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_inhabited [in bedrock.prelude.elpi.derive_test]
Deriving2Test.t3_eq_dec [in bedrock.prelude.elpi.derive_test]
Deriving2Test.Unnamed_thm1 [in bedrock.prelude.elpi.derive_test]
Deriving2Test.Unnamed_thm0 [in bedrock.prelude.elpi.derive_test]
Deriving2Test.Unnamed_thm [in bedrock.prelude.elpi.derive_test]
digit [in bedrock.prelude.parsec]
dropN [in bedrock.prelude.list_numbers]
E
encode_N [in bedrock.prelude.finite]enc_finite_N [in bedrock.prelude.finite]
Eq_Gt_discr [in bedrock.prelude.numbers]
Eq_Lt_discr [in bedrock.prelude.numbers]
Error.exc [in bedrock.prelude.error]
Error.t [in bedrock.prelude.error]
exact_char [in bedrock.prelude.parsec]
exact_bs [in bedrock.prelude.parsec]
F
FiniteTest.feature_finite [in bedrock.prelude.elpi.derive_test]FiniteTest.feature_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
FiniteTest.feature_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
FiniteTest.feature_eq_dec [in bedrock.prelude.elpi.derive_test]
FiniteTest.feature.t [in bedrock.prelude.elpi.derive_test]
FiniteTest.feature.to_N [in bedrock.prelude.elpi.derive_test]
FiniteTest.feature.t_finite [in bedrock.prelude.elpi.derive_test]
FiniteTest.feature.t_eq_dec [in bedrock.prelude.elpi.derive_test]
FiniteTest.Unnamed_thm1 [in bedrock.prelude.elpi.derive_test]
FiniteTest.Unnamed_thm0 [in bedrock.prelude.elpi.derive_test]
FiniteTest.Unnamed_thm [in bedrock.prelude.elpi.derive_test]
finite_bits_aux.mask_top [in bedrock.prelude.finite]
finite_bits_aux.masked_opt [in bedrock.prelude.finite]
finite_bits_aux.masked [in bedrock.prelude.finite]
finite_bits_aux.internal.to_bits_comm [in bedrock.prelude.finite]
finite_bits_aux.internal.to_bits_alt [in bedrock.prelude.finite]
finite_bits_aux.to_bits [in bedrock.prelude.finite]
finite_bits_aux.of_bits [in bedrock.prelude.finite]
finite_bits_aux.t [in bedrock.prelude.finite]
finite_bitmask_type_mixin.setbit [in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_list [in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_list_aux [in bedrock.prelude.finite]
finite_bitmask_type_mixin.filter [in bedrock.prelude.finite]
finite_bitmask_type_mixin.testbit [in bedrock.prelude.finite]
finite_bitmask_type_mixin.to_bitmask [in bedrock.prelude.finite]
finite_type_mixin.of_N [in bedrock.prelude.finite]
finite_type_mixin.to_N [in bedrock.prelude.finite]
finite_type_mixin.t_countable [in bedrock.prelude.finite]
finite_encoded_type_mixin.of_N [in bedrock.prelude.finite]
finite_preimage_set [in bedrock.prelude.finite]
finite_inverse [in bedrock.prelude.finite]
finite_preimage [in bedrock.prelude.finite]
fin_prod.update [in bedrock.prelude.finite_prod]
fin_prod.fmapO [in bedrock.prelude.finite_prod]
fin_prod.fmap [in bedrock.prelude.finite_prod]
fin_prod.lookup [in bedrock.prelude.finite_prod]
fin_prod.to_list [in bedrock.prelude.finite_prod]
fin_prod.internal.update' [in bedrock.prelude.finite_prod]
fin_prod.internal.lookup' [in bedrock.prelude.finite_prod]
fin_prod.internal.fmapO' [in bedrock.prelude.finite_prod]
fin_prod.internal.fmap' [in bedrock.prelude.finite_prod]
fin_prod.internal.to_list' [in bedrock.prelude.finite_prod]
fin.decode [in bedrock.prelude.fin]
fin.mk [in bedrock.prelude.fin]
fin.of_idx_fin' [in bedrock.prelude.fin]
fin.of_nat [in bedrock.prelude.fin]
fin.of_N [in bedrock.prelude.fin]
fin.of_nat' [in bedrock.prelude.fin]
fin.of_N' [in bedrock.prelude.fin]
fin.seq [in bedrock.prelude.fin]
fin.succ [in bedrock.prelude.fin]
fin.t [in bedrock.prelude.fin]
fin.to_idx_fin' [in bedrock.prelude.fin]
fin.to_N [in bedrock.prelude.fin]
fin.t_eq [in bedrock.prelude.fin]
fin.Unnamed_thm [in bedrock.prelude.fin]
fin.Unnamed_thm [in bedrock.prelude.fin]
fin.weaken_bool_decide [in bedrock.prelude.fin]
fin.weaken' [in bedrock.prelude.fin]
fin.zero [in bedrock.prelude.fin]
flip2 [in bedrock.prelude.base]
FMapExtra.MIXIN_LEIBNIZ.find_any [in bedrock.prelude.avl]
FMapExtra.MIXIN.build [in bedrock.prelude.avl]
FMapExtra.MIXIN.check_canon [in bedrock.prelude.avl]
FMapExtra.MIXIN.from_raw [in bedrock.prelude.avl]
FMapExtra.MIXIN.from_raw_or [in bedrock.prelude.avl]
FMapExtra.MIXIN.map_canon [in bedrock.prelude.avl]
FMapExtra.RAW.bst_sind [in bedrock.prelude.avl]
FMapExtra.RAW.bst_ind [in bedrock.prelude.avl]
FMapExtra.RAW.gt_tree [in bedrock.prelude.avl]
FMapExtra.RAW.In_sind [in bedrock.prelude.avl]
FMapExtra.RAW.In_ind [in bedrock.prelude.avl]
FMapExtra.RAW.lt_tree [in bedrock.prelude.avl]
FMapExtra.RAW.tree_sind [in bedrock.prelude.avl]
FMapExtra.RAW.tree_rec [in bedrock.prelude.avl]
FMapExtra.RAW.tree_ind [in bedrock.prelude.avl]
FMapExtra.RAW.tree_rect [in bedrock.prelude.avl]
ForallT_true [in bedrock.prelude.list]
ForallT_sind [in bedrock.prelude.list]
ForallT_rec [in bedrock.prelude.list]
ForallT_ind [in bedrock.prelude.list]
ForallT_rect [in bedrock.prelude.list]
force_some [in bedrock.prelude.option]
G
get_range_bits_fin [in bedrock.prelude.bitsN]get_range_bitsN [in bedrock.prelude.bitsN]
get_some [in bedrock.prelude.option]
gset_bind [in bedrock.prelude.gmap]
Gt_Lt_discr [in bedrock.prelude.numbers]
Gt_Eq_discr [in bedrock.prelude.numbers]
H
head_list [in bedrock.prelude.list_numbers]I
ignore_ws [in bedrock.prelude.parsec]initialIntConfig [in bedrock.prelude.interrupts]
insertN_simpl [in bedrock.prelude.list_numbers]
insertZ_simpl [in bedrock.prelude.list_numbers]
intcfg_valid [in bedrock.prelude.interrupts]
InteropTests.T1_finite [in bedrock.prelude.elpi.derive_test]
InteropTests.T1_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
InteropTests.T1_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
InteropTests.T2_eq_dec [in bedrock.prelude.elpi.derive_test]
int_types_match [in bedrock.prelude.interrupts]
int_trigger_match [in bedrock.prelude.interrupts]
INT_config_of [in bedrock.prelude.interrupts]
iso.inv [in bedrock.prelude.lens]
iso2lens [in bedrock.prelude.lens]
isSome [in bedrock.prelude.option]
L
lengthN [in bedrock.prelude.list_numbers]lengthN_simplZ [in bedrock.prelude.list_numbers]
lengthN_simpl [in bedrock.prelude.list_numbers]
lens_aux_1.lens.of_get_put [in bedrock.prelude.lens]
lens_aux_1.lens.of_get_set [in bedrock.prelude.lens]
Lens_with [in bedrock.prelude.elpi.derive.lens]
Level [in bedrock.prelude.page]
liftM2 [in bedrock.prelude.base]
lookupN_simpl [in bedrock.prelude.list_numbers]
lookupZ_simpl [in bedrock.prelude.list_numbers]
lookup_from_ctorlist [in bedrock.prelude.elpi.derive.countable]
Lt_Eq_discr [in bedrock.prelude.numbers]
Lt_Gt_discr [in bedrock.prelude.numbers]
N
NamedBinder [in bedrock.prelude.named_binder]N_to_Qp [in bedrock.prelude.numbers]
O
option.existsb [in bedrock.prelude.option]option.on [in bedrock.prelude.option]
OT_bs.eq_dec [in bedrock.prelude.bytestring_core]
OT_bs.compare [in bedrock.prelude.bytestring_core]
OT_bs.lt [in bedrock.prelude.bytestring_core]
OT_bs.eq [in bedrock.prelude.bytestring_core]
OT_bs.t [in bedrock.prelude.bytestring_core]
OT_byte.eq_dec [in bedrock.prelude.bytestring_core]
OT_byte.compare [in bedrock.prelude.bytestring_core]
OT_byte.lt [in bedrock.prelude.bytestring_core]
OT_byte.eq [in bedrock.prelude.bytestring_core]
OT_byte.t [in bedrock.prelude.bytestring_core]
P
paddr [in bedrock.prelude.addr]page_offset [in bedrock.prelude.page]
page_offset_of [in bedrock.prelude.page]
page_align_up [in bedrock.prelude.page]
page_align_dn [in bedrock.prelude.page]
PAGE_SIZE [in bedrock.prelude.page]
PAGE_BITS [in bedrock.prelude.page]
pairwise_disj_funs [in bedrock.prelude.list]
Pos.compare_eq [in bedrock.prelude.numbers]
Pos.compare_cont_eq [in bedrock.prelude.numbers]
Pos.compare_cont_not_Eq_mono [in bedrock.prelude.numbers]
pow2N [in bedrock.prelude.numbers]
pow2N_eq [in bedrock.prelude.numbers]
pow2N_aux [in bedrock.prelude.numbers]
pow2N_def [in bedrock.prelude.numbers]
Q
qPAGE_SIZE [in bedrock.prelude.page]Qp.add_all [in bedrock.prelude.numbers]
Qp.sub_all [in bedrock.prelude.numbers]
quoted [in bedrock.prelude.parsec]
R
rangeZ [in bedrock.prelude.list_numbers]rangeZ' [in bedrock.prelude.list_numbers]
reachable_sind [in bedrock.prelude.sts]
reachable_ind [in bedrock.prelude.sts]
replicateN [in bedrock.prelude.list_numbers]
replicateN_simpl [in bedrock.prelude.list_numbers]
resizeN [in bedrock.prelude.list_numbers]
rotateN [in bedrock.prelude.list_numbers]
rotateN_simpl [in bedrock.prelude.list_numbers]
round_up [in bedrock.prelude.numbers]
round_down [in bedrock.prelude.numbers]
run_full_bs [in bedrock.prelude.parsec]
run_bs [in bedrock.prelude.parsec]
S
same_property [in bedrock.prelude.option]seqN [in bedrock.prelude.list_numbers]
seqW [in bedrock.prelude.wrap]
set_rangeZ [in bedrock.prelude.fin_sets]
set_concat_map [in bedrock.prelude.fin_sets]
SimpleBitsetTest.feature_finite [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature_eq_dec [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature.t [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature.t_finite [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.feature.t_eq_dec [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.Unnamed_thm1 [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.Unnamed_thm0 [in bedrock.prelude.elpi.derive_test]
SimpleBitsetTest.Unnamed_thm [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_eq_dec [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite_subproof_elem_of [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_finite_subproof_nodup [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature_eq_dec [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t_finite [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t_eq_dec [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t_finite [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.feature.t_eq_dec [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.Unnamed_thm0 [in bedrock.prelude.elpi.derive_test]
SimpleFiniteTest.Unnamed_thm [in bedrock.prelude.elpi.derive_test]
simple_finite_bitmask_type_mixin.all_bits [in bedrock.prelude.finite]
sliceZ [in bedrock.prelude.list_numbers]
some_Forall2_unlock_subterm [in bedrock.prelude.option]
some_Forall2.unlock [in bedrock.prelude.option]
some_Forall2.body [in bedrock.prelude.option]
Sts.hide [in bedrock.prelude.sts]
Sts.init_state [in bedrock.prelude.sts]
Sts.map [in bedrock.prelude.sts]
Sts.par [in bedrock.prelude.sts]
Sts.State [in bedrock.prelude.sts]
Sts.step [in bedrock.prelude.sts]
Sts.step_star_ext [in bedrock.prelude.sts]
Sts.step_star_tau [in bedrock.prelude.sts]
Sts.step_star [in bedrock.prelude.sts]
sum.existsb [in bedrock.prelude.sum]
T
takeN [in bedrock.prelude.list_numbers]TCAndT_sind [in bedrock.prelude.tc_cond_type]
TCAndT_rec [in bedrock.prelude.tc_cond_type]
TCAndT_ind [in bedrock.prelude.tc_cond_type]
TCAndT_rect [in bedrock.prelude.tc_cond_type]
TCForceEq_sind [in bedrock.prelude.named_binder]
TCForceEq_rec [in bedrock.prelude.named_binder]
TCForceEq_ind [in bedrock.prelude.named_binder]
TCForceEq_rect [in bedrock.prelude.named_binder]
TCOrT_sind [in bedrock.prelude.tc_cond_type]
TCOrT_rec [in bedrock.prelude.tc_cond_type]
TCOrT_ind [in bedrock.prelude.tc_cond_type]
TCOrT_rect [in bedrock.prelude.tc_cond_type]
tele_arg_append [in bedrock.prelude.telescopes]
tele_bind_append [in bedrock.prelude.telescopes]
tele_arg_snoc [in bedrock.prelude.telescopes]
tele_bind_snoc [in bedrock.prelude.telescopes]
tele_snoc [in bedrock.prelude.telescopes]
tele_fun_pointwise [in bedrock.prelude.telescopes]
tele_append [in bedrock.prelude.telescopes]
Test.Unnamed_thm [in bedrock.prelude.named_binder]
Test.Unnamed_thm [in bedrock.prelude.named_binder]
V
vaddr [in bedrock.prelude.addr]W
wrapN_succ [in bedrock.prelude.wrap]wrapper.of_N [in bedrock.prelude.wrap]
wrapper.t [in bedrock.prelude.wrap]
wrapper.to_N [in bedrock.prelude.wrap]
ws [in bedrock.prelude.parsec]
Z
Zarith_simpl [in bedrock.prelude.list_numbers]_
_constr [in bedrock.prelude.lens]_total_fun [in bedrock.prelude.lens]
_apply [in bedrock.prelude.lens]
_map_apply [in bedrock.prelude.lens]
_lift [in bedrock.prelude.lens]
_const [in bedrock.prelude.lens]
_snd [in bedrock.prelude.lens]
_fst [in bedrock.prelude.lens]
_id [in bedrock.prelude.lens]
_bit [in bedrock.prelude.lens]
other
π_set [in bedrock.prelude.propset]Record Index
A
attrs.t [in bedrock.prelude.page]B
Binder [in bedrock.prelude.named_binder]C
Compare [in bedrock.prelude.base]Comparison [in bedrock.prelude.base]
Compose.config [in bedrock.prelude.sts]
F
FMapExtra.MAP.bst [in bedrock.prelude.avl]FMapExtra.RAW.triple [in bedrock.prelude.avl]
I
IdOfBS [in bedrock.prelude.named_binder]IntAction [in bedrock.prelude.interrupts]
IntConfig [in bedrock.prelude.interrupts]
IntLines [in bedrock.prelude.interrupts]
iso.lawsT [in bedrock.prelude.lens]
iso.t [in bedrock.prelude.lens]
L
LensLaws' [in bedrock.prelude.lens]N
Names [in bedrock.prelude.name]NNonZero [in bedrock.prelude.base]
P
PairwiseDisjoint [in bedrock.prelude.base]PossiblyEmptyNames [in bedrock.prelude.name]
S
Sts.sts [in bedrock.prelude.sts]Sts.t [in bedrock.prelude.sts]
T
ToBit [in bedrock.prelude.elpi.derive.bitset]ToN [in bedrock.prelude.elpi.derive.finite_type]
W
WrapN [in bedrock.prelude.wrap]wrapN_notations.WrapNAdd [in bedrock.prelude.wrap]
| 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 | (2322 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 | (89 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 | (102 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 | (116 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 | (59 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 | (765 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 | (97 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 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 | (50 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 | (43 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 | (91 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 | (342 entries) |
| Abbreviation 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 | (107 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 | (425 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 | (24 entries) |