| 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 | (536 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 | (2 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 | (5 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 | (24 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 | (3 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 | (1 entry) |
| 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 | (330 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 | (6 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 | (3 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 | (7 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 | (4 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 | (151 entries) |
Global Index
B
bin_Desc0 [lemma, in IntSetProofs]bitmapInRange [definition, in IntSetProofs]
bitmapInRange_bitmapOf [lemma, in IntSetProofs]
bitmapInRange_land [lemma, in IntSetProofs]
bitmapInRange_lxor [lemma, in IntSetProofs]
bitmapInRange_0 [lemma, in IntSetProofs]
bitmapInRange_outside [lemma, in IntSetProofs]
bit_diff_not_in_range [lemma, in IntSetProofs]
branchMask_spec [lemma, in IntSetProofs]
C
commonRange [definition, in IntSetProofs]commonRangeDisj [definition, in IntSetProofs]
commonRangeDisj_rBits_Different [lemma, in IntSetProofs]
commonRangeDisj_rNonneg [lemma, in IntSetProofs]
commonRangeDisj_rBits_pos [lemma, in IntSetProofs]
commonRangeDisj_sym [lemma, in IntSetProofs]
commonRangeDis_larger_r [lemma, in IntSetProofs]
commonRangeDis_larger_l [lemma, in IntSetProofs]
commonRange_sym [lemma, in IntSetProofs]
commonRange_idem [lemma, in IntSetProofs]
common_of_halves [lemma, in IntSetProofs]
D
deleteBM_Desc [lemma, in IntSetProofs]delete_WF [lemma, in IntSetProofs]
delete_Sem [lemma, in IntSetProofs]
delete_Desc [lemma, in IntSetProofs]
Desc [inductive, in IntSetProofs]
DescBin [constructor, in IntSetProofs]
DescBin' [lemma, in IntSetProofs]
DescSem [constructor, in IntSetProofs]
DescTip [constructor, in IntSetProofs]
Desc_has_member [lemma, in IntSetProofs]
Desc_some_f [lemma, in IntSetProofs]
Desc_neg_false [lemma, in IntSetProofs]
Desc_outside [lemma, in IntSetProofs]
Desc_larger_WIDTH [lemma, in IntSetProofs]
Desc_rNonneg [lemma, in IntSetProofs]
Desc_Desc0 [lemma, in IntSetProofs]
Desc_change_f [lemma, in IntSetProofs]
Desc0 [inductive, in IntSetProofs]
Desc0Nil [constructor, in IntSetProofs]
Desc0NotNil [constructor, in IntSetProofs]
Desc0_subRange [lemma, in IntSetProofs]
Desc0_neg_false [lemma, in IntSetProofs]
Desc0_outside [lemma, in IntSetProofs]
Desc0_WF [lemma, in IntSetProofs]
Desc0_Sem [lemma, in IntSetProofs]
different_prefix_same_bits_disjoint [lemma, in IntSetProofs]
different_prefix_same_bits_not_subrange [lemma, in IntSetProofs]
disjoint_commonRange [lemma, in IntSetProofs]
disjoint_rPrefix_differ [lemma, in IntSetProofs]
F
FIXME [axiom, in MapProofs]Foo [module, in MapProofs]
Foo [module, in SetProofs]
Foo [module, in IntSetProofs]
Foo.add [definition, in MapProofs]
Foo.add [definition, in SetProofs]
Foo.add [definition, in IntSetProofs]
Foo.add_3 [definition, in MapProofs]
Foo.add_2 [definition, in MapProofs]
Foo.add_1 [definition, in MapProofs]
Foo.add_3 [lemma, in SetProofs]
Foo.add_2 [lemma, in SetProofs]
Foo.add_1 [lemma, in SetProofs]
Foo.add_3 [lemma, in IntSetProofs]
Foo.add_2 [lemma, in IntSetProofs]
Foo.add_1 [lemma, in IntSetProofs]
Foo.balanced_size_constraints [lemma, in SetProofs]
Foo.balanced_children [lemma, in SetProofs]
Foo.balanceL_WF [lemma, in SetProofs]
Foo.balanceL_validsize [lemma, in SetProofs]
Foo.balanceL_ordered [lemma, in SetProofs]
Foo.balanceL_balanced [lemma, in SetProofs]
Foo.balanceL_add_size [lemma, in SetProofs]
Foo.balanceR_WF [lemma, in SetProofs]
Foo.balanceR_validsize [lemma, in SetProofs]
Foo.balanceR_ordered [lemma, in SetProofs]
Foo.balanceR_balanced [lemma, in SetProofs]
Foo.balanceR_add_size [lemma, in SetProofs]
Foo.before_ordered [definition, in SetProofs]
Foo.before_balancedR [definition, in SetProofs]
Foo.before_balancedL [definition, in SetProofs]
Foo.bin_compat [lemma, in SetProofs]
Foo.bin_not_empty [lemma, in SetProofs]
Foo.bounded_impl_right_const_true [lemma, in SetProofs]
Foo.bounded_impl_left_const_true [lemma, in SetProofs]
Foo.cardinal [definition, in MapProofs]
Foo.cardinal [definition, in SetProofs]
Foo.cardinal [definition, in IntSetProofs]
Foo.cardinal_1 [definition, in MapProofs]
Foo.cardinal_1 [lemma, in SetProofs]
Foo.cardinal_1 [lemma, in IntSetProofs]
Foo.choose [definition, in SetProofs]
Foo.choose [definition, in IntSetProofs]
Foo.choose_2 [lemma, in SetProofs]
Foo.choose_1 [lemma, in SetProofs]
Foo.choose_2 [lemma, in IntSetProofs]
Foo.choose_1 [lemma, in IntSetProofs]
Foo.compare [definition, in SetProofs]
Foo.diff [definition, in SetProofs]
Foo.diff [definition, in IntSetProofs]
Foo.diff_3 [lemma, in SetProofs]
Foo.diff_2 [lemma, in SetProofs]
Foo.diff_1 [lemma, in SetProofs]
Foo.diff_3 [lemma, in IntSetProofs]
Foo.diff_2 [lemma, in IntSetProofs]
Foo.diff_1 [lemma, in IntSetProofs]
Foo.elements [definition, in MapProofs]
Foo.elements [definition, in SetProofs]
Foo.elements [definition, in IntSetProofs]
Foo.elements_3w [definition, in MapProofs]
Foo.elements_2 [definition, in MapProofs]
Foo.elements_1 [definition, in MapProofs]
Foo.elements_3w [lemma, in SetProofs]
Foo.elements_2 [lemma, in SetProofs]
Foo.elements_1 [lemma, in SetProofs]
Foo.elements_3w [lemma, in IntSetProofs]
Foo.elements_2 [lemma, in IntSetProofs]
Foo.elements_1 [lemma, in IntSetProofs]
Foo.elt [definition, in SetProofs]
Foo.elt [definition, in IntSetProofs]
Foo.elt_compare_eq [lemma, in SetProofs]
Foo.elt_compare_gt [lemma, in SetProofs]
Foo.elt_compare_lt [lemma, in SetProofs]
Foo.elt_gt [lemma, in SetProofs]
Foo.elt_lt [lemma, in SetProofs]
Foo.elt_compare_eq'P [lemma, in SetProofs]
Foo.elt_compare_eqP [lemma, in SetProofs]
Foo.elt_compare_gt'P [lemma, in SetProofs]
Foo.elt_compare_gtP [lemma, in SetProofs]
Foo.elt_compare_lt'P [lemma, in SetProofs]
Foo.elt_compare_ltP [lemma, in SetProofs]
Foo.elt_gtP [lemma, in SetProofs]
Foo.elt_ltP [lemma, in SetProofs]
Foo.Empty [definition, in MapProofs]
Foo.empty [definition, in MapProofs]
Foo.empty [definition, in SetProofs]
Foo.Empty [definition, in SetProofs]
Foo.empty [definition, in IntSetProofs]
Foo.Empty [definition, in IntSetProofs]
Foo.empty_1 [definition, in MapProofs]
Foo.empty_not_bin [lemma, in SetProofs]
Foo.empty_1 [lemma, in SetProofs]
Foo.empty_1 [lemma, in IntSetProofs]
Foo.eq [definition, in SetProofs]
Foo.eq [definition, in IntSetProofs]
Foo.Equal [definition, in MapProofs]
Foo.equal [definition, in MapProofs]
Foo.equal [definition, in SetProofs]
Foo.Equal [definition, in SetProofs]
Foo.equal [definition, in IntSetProofs]
Foo.Equal [definition, in IntSetProofs]
Foo.equal_2 [definition, in MapProofs]
Foo.equal_1 [definition, in MapProofs]
Foo.equal_2 [lemma, in SetProofs]
Foo.equal_1 [lemma, in SetProofs]
Foo.Equal_set [definition, in SetProofs]
Foo.equal_2 [lemma, in IntSetProofs]
Foo.equal_1 [lemma, in IntSetProofs]
Foo.Equal_set [definition, in IntSetProofs]
Foo.Equiv [definition, in MapProofs]
Foo.Equivb [definition, in MapProofs]
Foo.eq_key_elt [definition, in MapProofs]
Foo.eq_key [definition, in MapProofs]
Foo.Eq_t [instance, in MapProofs]
Foo.eq_trans [lemma, in SetProofs]
Foo.eq_set_trans [lemma, in SetProofs]
Foo.eq_sym [lemma, in SetProofs]
Foo.eq_set_sym [lemma, in SetProofs]
Foo.eq_refl [lemma, in SetProofs]
Foo.eq_set_refl [lemma, in SetProofs]
Foo.eq_dec [definition, in SetProofs]
Foo.eq_set [definition, in SetProofs]
Foo.Eq_t [instance, in SetProofs]
Foo.eq_trans [lemma, in IntSetProofs]
Foo.eq_set_trans [lemma, in IntSetProofs]
Foo.eq_sym [lemma, in IntSetProofs]
Foo.eq_set_sym [lemma, in IntSetProofs]
Foo.eq_refl [lemma, in IntSetProofs]
Foo.eq_set_refl [lemma, in IntSetProofs]
Foo.eq_dec [definition, in IntSetProofs]
Foo.eq_set [definition, in IntSetProofs]
Foo.Exists [definition, in SetProofs]
Foo.Exists [definition, in IntSetProofs]
Foo.exists_2 [lemma, in SetProofs]
Foo.exists_1 [lemma, in SetProofs]
Foo.exists_ [definition, in SetProofs]
Foo.exists_2 [lemma, in IntSetProofs]
Foo.exists_1 [lemma, in IntSetProofs]
Foo.exists_ [definition, in IntSetProofs]
Foo.filter [definition, in SetProofs]
Foo.filter [definition, in IntSetProofs]
Foo.filter_3 [lemma, in SetProofs]
Foo.filter_2 [lemma, in SetProofs]
Foo.filter_1 [lemma, in SetProofs]
Foo.filter_3 [lemma, in IntSetProofs]
Foo.filter_2 [lemma, in IntSetProofs]
Foo.filter_1 [lemma, in IntSetProofs]
Foo.find [definition, in MapProofs]
Foo.find_2 [definition, in MapProofs]
Foo.find_1 [definition, in MapProofs]
Foo.fold [definition, in MapProofs]
Foo.fold [definition, in SetProofs]
Foo.fold [definition, in IntSetProofs]
Foo.fold_1 [definition, in MapProofs]
Foo.fold_1 [lemma, in SetProofs]
Foo.fold_1 [lemma, in IntSetProofs]
Foo.for_all_2 [lemma, in SetProofs]
Foo.for_all_1 [lemma, in SetProofs]
Foo.for_all [definition, in SetProofs]
Foo.For_all [definition, in SetProofs]
Foo.for_all_2 [lemma, in IntSetProofs]
Foo.for_all_1 [lemma, in IntSetProofs]
Foo.for_all [definition, in IntSetProofs]
Foo.For_all [definition, in IntSetProofs]
Foo.In [definition, in MapProofs]
Foo.In [definition, in SetProofs]
Foo.In [definition, in IntSetProofs]
Foo.insert_prop [lemma, in SetProofs]
Foo.inset_destruct [lemma, in SetProofs]
Foo.inset_balanceR [lemma, in SetProofs]
Foo.inset_balanceL [lemma, in SetProofs]
Foo.inter [definition, in SetProofs]
Foo.inter [definition, in IntSetProofs]
Foo.inter_3 [lemma, in SetProofs]
Foo.inter_2 [lemma, in SetProofs]
Foo.inter_1 [lemma, in SetProofs]
Foo.inter_3 [lemma, in IntSetProofs]
Foo.inter_2 [lemma, in IntSetProofs]
Foo.inter_1 [lemma, in IntSetProofs]
Foo.In_1 [lemma, in SetProofs]
Foo.In_set [definition, in SetProofs]
Foo.In_1 [lemma, in IntSetProofs]
Foo.In_set [definition, in IntSetProofs]
Foo.is_empty_2 [definition, in MapProofs]
Foo.is_empty_1 [definition, in MapProofs]
Foo.is_empty [definition, in MapProofs]
Foo.is_empty_2 [lemma, in SetProofs]
Foo.is_empty_1 [lemma, in SetProofs]
Foo.is_empty [definition, in SetProofs]
Foo.is_empty_2 [lemma, in IntSetProofs]
Foo.is_empty_1 [lemma, in IntSetProofs]
Foo.is_empty [definition, in IntSetProofs]
Foo.key [definition, in MapProofs]
Foo.local_realsize [definition, in SetProofs]
Foo.local_bounded_size_irrelevance [lemma, in SetProofs]
Foo.local_bounded_constr [lemma, in SetProofs]
Foo.local_bounded_right_relax [lemma, in SetProofs]
Foo.local_bounded_left_relax [lemma, in SetProofs]
Foo.local_bounded [definition, in SetProofs]
Foo.map [definition, in MapProofs]
Foo.mapi [definition, in MapProofs]
Foo.mapi_2 [definition, in MapProofs]
Foo.mapi_1 [definition, in MapProofs]
Foo.MapsTo [definition, in MapProofs]
Foo.MapsTo_1 [definition, in MapProofs]
Foo.map_2 [definition, in MapProofs]
Foo.map_1 [definition, in MapProofs]
Foo.map2 [definition, in MapProofs]
Foo.map2_2 [definition, in MapProofs]
Foo.map2_1 [definition, in MapProofs]
Foo.mem [definition, in MapProofs]
Foo.mem [definition, in SetProofs]
Foo.mem [definition, in IntSetProofs]
Foo.mem_2 [definition, in MapProofs]
Foo.mem_1 [definition, in MapProofs]
Foo.mem_2 [lemma, in SetProofs]
Foo.mem_1 [lemma, in SetProofs]
Foo.mem_2 [lemma, in IntSetProofs]
Foo.mem_1 [lemma, in IntSetProofs]
Foo.ordered_rewrite [lemma, in SetProofs]
Foo.ordered_children [lemma, in SetProofs]
Foo.OrdFacts [module, in SetProofs]
Foo.OrdFacts [module, in IntSetProofs]
Foo.Ord_t [instance, in MapProofs]
Foo.Ord_t [instance, in SetProofs]
Foo.pack [definition, in MapProofs]
Foo.pack [definition, in SetProofs]
Foo.pack [definition, in IntSetProofs]
Foo.partial_gt_relax [lemma, in SetProofs]
Foo.partial_gt_mono [lemma, in SetProofs]
Foo.partial_lt_relax [lemma, in SetProofs]
Foo.partial_lt_mono [lemma, in SetProofs]
Foo.partial_gt [definition, in SetProofs]
Foo.partial_lt [definition, in SetProofs]
Foo.partition [definition, in SetProofs]
Foo.partition [definition, in IntSetProofs]
Foo.partition_2 [lemma, in SetProofs]
Foo.partition_1 [lemma, in SetProofs]
Foo.partition_2 [lemma, in IntSetProofs]
Foo.partition_1 [lemma, in IntSetProofs]
Foo.remove [definition, in MapProofs]
Foo.remove [definition, in SetProofs]
Foo.remove [definition, in IntSetProofs]
Foo.remove_3 [definition, in MapProofs]
Foo.remove_2 [definition, in MapProofs]
Foo.remove_1 [definition, in MapProofs]
Foo.remove_3 [lemma, in SetProofs]
Foo.remove_2 [lemma, in SetProofs]
Foo.remove_1 [lemma, in SetProofs]
Foo.remove_3 [lemma, in IntSetProofs]
Foo.remove_2 [lemma, in IntSetProofs]
Foo.remove_1 [lemma, in IntSetProofs]
Foo.singleton [definition, in SetProofs]
Foo.singleton [definition, in IntSetProofs]
Foo.singleton_2 [lemma, in SetProofs]
Foo.singleton_1 [lemma, in SetProofs]
Foo.singleton_2 [lemma, in IntSetProofs]
Foo.singleton_1 [lemma, in IntSetProofs]
Foo.size_irrelevance_in_ordered [lemma, in SetProofs]
Foo.subset [definition, in SetProofs]
Foo.Subset [definition, in SetProofs]
Foo.subset [definition, in IntSetProofs]
Foo.Subset [definition, in IntSetProofs]
Foo.subset_2 [lemma, in SetProofs]
Foo.subset_1 [lemma, in SetProofs]
Foo.subset_2 [lemma, in IntSetProofs]
Foo.subset_1 [lemma, in IntSetProofs]
Foo.t [definition, in MapProofs]
Foo.t [section, in MapProofs]
Foo.t [definition, in SetProofs]
Foo.t [definition, in IntSetProofs]
Foo.Types [section, in MapProofs]
Foo.Types.elt [variable, in MapProofs]
Foo.Types.elt' [variable, in MapProofs]
Foo.Types.elt'' [variable, in MapProofs]
Foo.Types.Spec [section, in MapProofs]
Foo.Types.Spec.cmp [variable, in MapProofs]
Foo.Types.Spec.e [variable, in MapProofs]
Foo.Types.Spec.e' [variable, in MapProofs]
Foo.Types.Spec.m [variable, in MapProofs]
Foo.Types.Spec.m' [variable, in MapProofs]
Foo.Types.Spec.m'' [variable, in MapProofs]
Foo.Types.Spec.x [variable, in MapProofs]
Foo.Types.Spec.y [variable, in MapProofs]
Foo.Types.Spec.z [variable, in MapProofs]
Foo.t.elt [variable, in MapProofs]
Foo.union [definition, in SetProofs]
Foo.union [definition, in IntSetProofs]
Foo.union_3 [lemma, in SetProofs]
Foo.union_2 [lemma, in SetProofs]
Foo.union_1 [lemma, in SetProofs]
Foo.union_3 [lemma, in IntSetProofs]
Foo.union_2 [lemma, in IntSetProofs]
Foo.union_1 [lemma, in IntSetProofs]
Foo.validsize_children [lemma, in SetProofs]
Foo.WF [definition, in MapProofs]
Foo.WF [definition, in SetProofs]
Foo.WF_prop_r3 [lemma, in SetProofs]
Foo.WF_prop_l3 [lemma, in SetProofs]
Foo.WF_prop_r2 [lemma, in SetProofs]
Foo.WF_prop_l2 [lemma, in SetProofs]
Foo.WF_prop_r1 [lemma, in SetProofs]
Foo.WF_prop_l1 [lemma, in SetProofs]
Foo.WF_singleton [lemma, in SetProofs]
Foo.WF_validsize [lemma, in SetProofs]
Foo.WF_ordered [lemma, in SetProofs]
Foo.WF_balanced [lemma, in SetProofs]
Foo.WF_size_pos [lemma, in SetProofs]
Foo.WF_size_nonneg [lemma, in SetProofs]
Foo.WF_size_children [lemma, in SetProofs]
Foo.WF_children [lemma, in SetProofs]
_ <-- _ ;; _ [notation, in SetProofs]
_ <-- _ ;; _ [notation, in IntSetProofs]
H
halfRange [definition, in IntSetProofs]halfRange_smaller [lemma, in IntSetProofs]
halfRange_isSubrange_testbit [lemma, in IntSetProofs]
halfRange_inRange_testbit [lemma, in IntSetProofs]
halves_disj [lemma, in IntSetProofs]
halves_disj_aux [lemma, in IntSetProofs]
halves_disj_aux_aux [lemma, in IntSetProofs]
I
inRange [definition, in IntSetProofs]inRange_both_not_disj [lemma, in IntSetProofs]
inRange_both_smaller_subRange [lemma, in IntSetProofs]
inRange_isSubrange_false [lemma, in IntSetProofs]
inRange_isSubrange_true [lemma, in IntSetProofs]
insertBM_Desc [lemma, in IntSetProofs]
insert_WF [lemma, in IntSetProofs]
insert_Sem [lemma, in IntSetProofs]
insert_Nil_Desc [lemma, in IntSetProofs]
insert_Desc [lemma, in IntSetProofs]
intersection_WF [lemma, in IntSetProofs]
intersection_Sem [lemma, in IntSetProofs]
intersection_Desc [definition, in IntSetProofs]
intersection_eq [lemma, in IntSetProofs]
intersection_body [definition, in IntSetProofs]
IntSetProofs [library]
Int_is_Z [lemma, in SetProofs]
Int_eq_is_Z_eq [lemma, in SetProofs]
Int_ge_is_Z_ge [lemma, in SetProofs]
Int_gt_is_Z_gt [lemma, in SetProofs]
Int_le_is_Z_le [lemma, in SetProofs]
Int_lt_is_Z_lt [lemma, in SetProofs]
Int_mult_is_Z_mult [lemma, in SetProofs]
Int_minus_is_Z_minus [lemma, in SetProofs]
Int_plus_is_Z_plus [lemma, in SetProofs]
Int_And_Z.b [variable, in SetProofs]
Int_And_Z.a [variable, in SetProofs]
Int_And_Z [section, in SetProofs]
isBitMask [definition, in IntSetProofs]
isBitMask_bitmapOf [lemma, in IntSetProofs]
isBitMask_lor [lemma, in IntSetProofs]
isBitMask_testbit [lemma, in IntSetProofs]
isBitMask_isBitMask0 [lemma, in IntSetProofs]
isBitMask0 [definition, in IntSetProofs]
isBitMask0_lxor [lemma, in IntSetProofs]
isBitMask0_land [lemma, in IntSetProofs]
isBitMask0_zero_or_isBitMask [lemma, in IntSetProofs]
isSubrange [definition, in IntSetProofs]
isSubrange_commonRange [lemma, in IntSetProofs]
isSubrange_commonRange_r' [lemma, in IntSetProofs]
isSubrange_commonRange_l' [lemma, in IntSetProofs]
isSubrange_commonRange_l [lemma, in IntSetProofs]
isSubrange_commonRange_r [lemma, in IntSetProofs]
isSubrange_halfRange_commonRangeDisj [lemma, in IntSetProofs]
isSubrange_halfRange [lemma, in IntSetProofs]
isSubrange_disj_disj_l [lemma, in IntSetProofs]
isSubrange_disj_disj_r [lemma, in IntSetProofs]
isSubrange_antisym [lemma, in IntSetProofs]
isSubrange_trans [lemma, in IntSetProofs]
isSubrange_refl [lemma, in IntSetProofs]
isTipPrefix [definition, in IntSetProofs]
isTipPrefix_shiftl_shiftr [lemma, in IntSetProofs]
isTipPrefix_prefixOf [lemma, in IntSetProofs]
isTipPrefix_prefixMask [lemma, in IntSetProofs]
isTipPrefix_suffixMask [lemma, in IntSetProofs]
L
land_shiftl_ones [lemma, in IntSetProofs]land_pow2_eq [lemma, in IntSetProofs]
link_Desc [lemma, in IntSetProofs]
log2_le_lin' [lemma, in IntSetProofs]
log2_ones [lemma, in IntSetProofs]
lor_ones_ones [lemma, in IntSetProofs]
lxor_pos [lemma, in IntSetProofs]
M
MapProofs [library]mask_spec [lemma, in IntSetProofs]
mask_to_upper_bits [lemma, in IntSetProofs]
member_Sem [lemma, in IntSetProofs]
member_Desc0 [lemma, in IntSetProofs]
member_Desc [lemma, in IntSetProofs]
msDiffBit [section, in IntSetProofs]
msDiffBit [definition, in IntSetProofs]
msDiffBit_pos [lemma, in IntSetProofs]
msDiffBit_larger_r [lemma, in IntSetProofs]
msDiffBit_larger_l [lemma, in IntSetProofs]
msDiffBit_larger [lemma, in IntSetProofs]
msDiffBit_larger_tmp [lemma, in IntSetProofs]
msDiffBit_less [lemma, in IntSetProofs]
msDiffBit_shiftr_same [lemma, in IntSetProofs]
msDiffBit_Same [lemma, in IntSetProofs]
msDiffBit_Different [lemma, in IntSetProofs]
msDiffBit_sym [lemma, in IntSetProofs]
msDiffBit.Hne [variable, in IntSetProofs]
msDiffBit.Hnonneg1 [variable, in IntSetProofs]
msDiffBit.Hnonneg2 [variable, in IntSetProofs]
msDiffBit.p1 [variable, in IntSetProofs]
msDiffBit.p2 [variable, in IntSetProofs]
N
nomatch_zero_smaller [lemma, in IntSetProofs]nomatch_zero [lemma, in IntSetProofs]
nomatch_spec [lemma, in IntSetProofs]
N_land_pow2_testbit [lemma, in IntSetProofs]
N_pow_pos_nonneg [lemma, in IntSetProofs]
N_lt_pow2_testbits [lemma, in IntSetProofs]
N_gt_0_neq [lemma, in IntSetProofs]
O
of_N_shiftl [lemma, in IntSetProofs]of_N_log2 [lemma, in IntSetProofs]
ones_spec [lemma, in IntSetProofs]
ones_nonneg [lemma, in IntSetProofs]
option_int_eq [lemma, in SetProofs]
option_int_eqP [lemma, in SetProofs]
Option_Int.b [variable, in SetProofs]
Option_Int.a [variable, in SetProofs]
Option_Int [section, in SetProofs]
outside_commonRangeDisj_r [lemma, in IntSetProofs]
outside_commonRangeDisj_l [lemma, in IntSetProofs]
P
pos_pos [lemma, in IntSetProofs]pos_nonneg [lemma, in IntSetProofs]
prefixOf_eqb_spec [lemma, in IntSetProofs]
prefixOf_eq_shiftr [lemma, in IntSetProofs]
prefixOf_nonneg [lemma, in IntSetProofs]
R
range [definition, in IntSetProofs]rangeDisjoint [definition, in IntSetProofs]
rangeDisjoint_inRange_false [lemma, in IntSetProofs]
rangeDisjoint_sym [lemma, in IntSetProofs]
rBits [definition, in IntSetProofs]
rBits_halfRange [lemma, in IntSetProofs]
rMask [definition, in IntSetProofs]
rNonneg [definition, in IntSetProofs]
rNonneg_halfRange [lemma, in IntSetProofs]
rNonneg_subrange [lemma, in IntSetProofs]
rPrefix [definition, in IntSetProofs]
rPrefix_shiftr [lemma, in IntSetProofs]
rPrefix_inRange [lemma, in IntSetProofs]
rPrefix_rBits_range_eq [lemma, in IntSetProofs]
S
Sem [inductive, in IntSetProofs]SemNil [constructor, in IntSetProofs]
Sem_change_f [lemma, in IntSetProofs]
SetProofs [library]
shiftr_eq_ldiff [lemma, in IntSetProofs]
shorter_spec [lemma, in IntSetProofs]
singleton_WF [lemma, in IntSetProofs]
singleton_Sem [lemma, in IntSetProofs]
singleton_Desc [lemma, in IntSetProofs]
smaller_subRange_other_half [lemma, in IntSetProofs]
smaller_not_subrange_disjoint_iff [lemma, in IntSetProofs]
smaller_not_subrange_disjoint [lemma, in IntSetProofs]
smaller_inRange_iff_subRange [lemma, in IntSetProofs]
subRange_smaller [lemma, in IntSetProofs]
succ_nonneg [lemma, in IntSetProofs]
suffixOf_noneg [lemma, in IntSetProofs]
suffixOf_lt_WIDTH [lemma, in IntSetProofs]
T
testbit_halfRange [lemma, in IntSetProofs]testbit_halfRange_false_false [lemma, in IntSetProofs]
testbit_halfRange_isSubrange [lemma, in IntSetProofs]
testbit_halfRange_true [lemma, in IntSetProofs]
testbit_halfRange_true_false [lemma, in IntSetProofs]
testbit_halfRange_false [lemma, in IntSetProofs]
testbit_1 [lemma, in IntSetProofs]
tip_Desc0 [lemma, in IntSetProofs]
tip_widthZ [definition, in IntSetProofs]
tip_width [definition, in IntSetProofs]
to_N_log2 [lemma, in IntSetProofs]
U
union_WF [lemma, in IntSetProofs]union_Sem [lemma, in IntSetProofs]
union_Desc [definition, in IntSetProofs]
union_eq [lemma, in IntSetProofs]
union_body [definition, in IntSetProofs]
W
WF [definition, in IntSetProofs]WIDTH [definition, in IntSetProofs]
Z
zero_spec [lemma, in IntSetProofs]ZReflect [section, in SetProofs]
ZReflect.a [variable, in SetProofs]
ZReflect.b [variable, in SetProofs]
Z_gtP [lemma, in SetProofs]
Z_ltP [lemma, in SetProofs]
Z_eqP [lemma, in SetProofs]
Z_eq_shiftr_land_ones [lemma, in IntSetProofs]
Z_shiftl_injb [lemma, in IntSetProofs]
Z_shiftl_inj [lemma, in IntSetProofs]
Notation Index
F
_ <-- _ ;; _ [in SetProofs]_ <-- _ ;; _ [in IntSetProofs]
Module Index
F
Foo [in MapProofs]Foo [in SetProofs]
Foo [in IntSetProofs]
Foo.OrdFacts [in SetProofs]
Foo.OrdFacts [in IntSetProofs]
Variable Index
F
Foo.Types.elt [in MapProofs]Foo.Types.elt' [in MapProofs]
Foo.Types.elt'' [in MapProofs]
Foo.Types.Spec.cmp [in MapProofs]
Foo.Types.Spec.e [in MapProofs]
Foo.Types.Spec.e' [in MapProofs]
Foo.Types.Spec.m [in MapProofs]
Foo.Types.Spec.m' [in MapProofs]
Foo.Types.Spec.m'' [in MapProofs]
Foo.Types.Spec.x [in MapProofs]
Foo.Types.Spec.y [in MapProofs]
Foo.Types.Spec.z [in MapProofs]
Foo.t.elt [in MapProofs]
I
Int_And_Z.b [in SetProofs]Int_And_Z.a [in SetProofs]
M
msDiffBit.Hne [in IntSetProofs]msDiffBit.Hnonneg1 [in IntSetProofs]
msDiffBit.Hnonneg2 [in IntSetProofs]
msDiffBit.p1 [in IntSetProofs]
msDiffBit.p2 [in IntSetProofs]
O
Option_Int.b [in SetProofs]Option_Int.a [in SetProofs]
Z
ZReflect.a [in SetProofs]ZReflect.b [in SetProofs]
Library Index
I
IntSetProofsM
MapProofsS
SetProofsAxiom Index
F
FIXME [in MapProofs]Lemma Index
B
bin_Desc0 [in IntSetProofs]bitmapInRange_bitmapOf [in IntSetProofs]
bitmapInRange_land [in IntSetProofs]
bitmapInRange_lxor [in IntSetProofs]
bitmapInRange_0 [in IntSetProofs]
bitmapInRange_outside [in IntSetProofs]
bit_diff_not_in_range [in IntSetProofs]
branchMask_spec [in IntSetProofs]
C
commonRangeDisj_rBits_Different [in IntSetProofs]commonRangeDisj_rNonneg [in IntSetProofs]
commonRangeDisj_rBits_pos [in IntSetProofs]
commonRangeDisj_sym [in IntSetProofs]
commonRangeDis_larger_r [in IntSetProofs]
commonRangeDis_larger_l [in IntSetProofs]
commonRange_sym [in IntSetProofs]
commonRange_idem [in IntSetProofs]
common_of_halves [in IntSetProofs]
D
deleteBM_Desc [in IntSetProofs]delete_WF [in IntSetProofs]
delete_Sem [in IntSetProofs]
delete_Desc [in IntSetProofs]
DescBin' [in IntSetProofs]
Desc_has_member [in IntSetProofs]
Desc_some_f [in IntSetProofs]
Desc_neg_false [in IntSetProofs]
Desc_outside [in IntSetProofs]
Desc_larger_WIDTH [in IntSetProofs]
Desc_rNonneg [in IntSetProofs]
Desc_Desc0 [in IntSetProofs]
Desc_change_f [in IntSetProofs]
Desc0_subRange [in IntSetProofs]
Desc0_neg_false [in IntSetProofs]
Desc0_outside [in IntSetProofs]
Desc0_WF [in IntSetProofs]
Desc0_Sem [in IntSetProofs]
different_prefix_same_bits_disjoint [in IntSetProofs]
different_prefix_same_bits_not_subrange [in IntSetProofs]
disjoint_commonRange [in IntSetProofs]
disjoint_rPrefix_differ [in IntSetProofs]
F
Foo.add_3 [in SetProofs]Foo.add_2 [in SetProofs]
Foo.add_1 [in SetProofs]
Foo.add_3 [in IntSetProofs]
Foo.add_2 [in IntSetProofs]
Foo.add_1 [in IntSetProofs]
Foo.balanced_size_constraints [in SetProofs]
Foo.balanced_children [in SetProofs]
Foo.balanceL_WF [in SetProofs]
Foo.balanceL_validsize [in SetProofs]
Foo.balanceL_ordered [in SetProofs]
Foo.balanceL_balanced [in SetProofs]
Foo.balanceL_add_size [in SetProofs]
Foo.balanceR_WF [in SetProofs]
Foo.balanceR_validsize [in SetProofs]
Foo.balanceR_ordered [in SetProofs]
Foo.balanceR_balanced [in SetProofs]
Foo.balanceR_add_size [in SetProofs]
Foo.bin_compat [in SetProofs]
Foo.bin_not_empty [in SetProofs]
Foo.bounded_impl_right_const_true [in SetProofs]
Foo.bounded_impl_left_const_true [in SetProofs]
Foo.cardinal_1 [in SetProofs]
Foo.cardinal_1 [in IntSetProofs]
Foo.choose_2 [in SetProofs]
Foo.choose_1 [in SetProofs]
Foo.choose_2 [in IntSetProofs]
Foo.choose_1 [in IntSetProofs]
Foo.diff_3 [in SetProofs]
Foo.diff_2 [in SetProofs]
Foo.diff_1 [in SetProofs]
Foo.diff_3 [in IntSetProofs]
Foo.diff_2 [in IntSetProofs]
Foo.diff_1 [in IntSetProofs]
Foo.elements_3w [in SetProofs]
Foo.elements_2 [in SetProofs]
Foo.elements_1 [in SetProofs]
Foo.elements_3w [in IntSetProofs]
Foo.elements_2 [in IntSetProofs]
Foo.elements_1 [in IntSetProofs]
Foo.elt_compare_eq [in SetProofs]
Foo.elt_compare_gt [in SetProofs]
Foo.elt_compare_lt [in SetProofs]
Foo.elt_gt [in SetProofs]
Foo.elt_lt [in SetProofs]
Foo.elt_compare_eq'P [in SetProofs]
Foo.elt_compare_eqP [in SetProofs]
Foo.elt_compare_gt'P [in SetProofs]
Foo.elt_compare_gtP [in SetProofs]
Foo.elt_compare_lt'P [in SetProofs]
Foo.elt_compare_ltP [in SetProofs]
Foo.elt_gtP [in SetProofs]
Foo.elt_ltP [in SetProofs]
Foo.empty_not_bin [in SetProofs]
Foo.empty_1 [in SetProofs]
Foo.empty_1 [in IntSetProofs]
Foo.equal_2 [in SetProofs]
Foo.equal_1 [in SetProofs]
Foo.equal_2 [in IntSetProofs]
Foo.equal_1 [in IntSetProofs]
Foo.eq_trans [in SetProofs]
Foo.eq_set_trans [in SetProofs]
Foo.eq_sym [in SetProofs]
Foo.eq_set_sym [in SetProofs]
Foo.eq_refl [in SetProofs]
Foo.eq_set_refl [in SetProofs]
Foo.eq_trans [in IntSetProofs]
Foo.eq_set_trans [in IntSetProofs]
Foo.eq_sym [in IntSetProofs]
Foo.eq_set_sym [in IntSetProofs]
Foo.eq_refl [in IntSetProofs]
Foo.eq_set_refl [in IntSetProofs]
Foo.exists_2 [in SetProofs]
Foo.exists_1 [in SetProofs]
Foo.exists_2 [in IntSetProofs]
Foo.exists_1 [in IntSetProofs]
Foo.filter_3 [in SetProofs]
Foo.filter_2 [in SetProofs]
Foo.filter_1 [in SetProofs]
Foo.filter_3 [in IntSetProofs]
Foo.filter_2 [in IntSetProofs]
Foo.filter_1 [in IntSetProofs]
Foo.fold_1 [in SetProofs]
Foo.fold_1 [in IntSetProofs]
Foo.for_all_2 [in SetProofs]
Foo.for_all_1 [in SetProofs]
Foo.for_all_2 [in IntSetProofs]
Foo.for_all_1 [in IntSetProofs]
Foo.insert_prop [in SetProofs]
Foo.inset_destruct [in SetProofs]
Foo.inset_balanceR [in SetProofs]
Foo.inset_balanceL [in SetProofs]
Foo.inter_3 [in SetProofs]
Foo.inter_2 [in SetProofs]
Foo.inter_1 [in SetProofs]
Foo.inter_3 [in IntSetProofs]
Foo.inter_2 [in IntSetProofs]
Foo.inter_1 [in IntSetProofs]
Foo.In_1 [in SetProofs]
Foo.In_1 [in IntSetProofs]
Foo.is_empty_2 [in SetProofs]
Foo.is_empty_1 [in SetProofs]
Foo.is_empty_2 [in IntSetProofs]
Foo.is_empty_1 [in IntSetProofs]
Foo.local_bounded_size_irrelevance [in SetProofs]
Foo.local_bounded_constr [in SetProofs]
Foo.local_bounded_right_relax [in SetProofs]
Foo.local_bounded_left_relax [in SetProofs]
Foo.mem_2 [in SetProofs]
Foo.mem_1 [in SetProofs]
Foo.mem_2 [in IntSetProofs]
Foo.mem_1 [in IntSetProofs]
Foo.ordered_rewrite [in SetProofs]
Foo.ordered_children [in SetProofs]
Foo.partial_gt_relax [in SetProofs]
Foo.partial_gt_mono [in SetProofs]
Foo.partial_lt_relax [in SetProofs]
Foo.partial_lt_mono [in SetProofs]
Foo.partition_2 [in SetProofs]
Foo.partition_1 [in SetProofs]
Foo.partition_2 [in IntSetProofs]
Foo.partition_1 [in IntSetProofs]
Foo.remove_3 [in SetProofs]
Foo.remove_2 [in SetProofs]
Foo.remove_1 [in SetProofs]
Foo.remove_3 [in IntSetProofs]
Foo.remove_2 [in IntSetProofs]
Foo.remove_1 [in IntSetProofs]
Foo.singleton_2 [in SetProofs]
Foo.singleton_1 [in SetProofs]
Foo.singleton_2 [in IntSetProofs]
Foo.singleton_1 [in IntSetProofs]
Foo.size_irrelevance_in_ordered [in SetProofs]
Foo.subset_2 [in SetProofs]
Foo.subset_1 [in SetProofs]
Foo.subset_2 [in IntSetProofs]
Foo.subset_1 [in IntSetProofs]
Foo.union_3 [in SetProofs]
Foo.union_2 [in SetProofs]
Foo.union_1 [in SetProofs]
Foo.union_3 [in IntSetProofs]
Foo.union_2 [in IntSetProofs]
Foo.union_1 [in IntSetProofs]
Foo.validsize_children [in SetProofs]
Foo.WF_prop_r3 [in SetProofs]
Foo.WF_prop_l3 [in SetProofs]
Foo.WF_prop_r2 [in SetProofs]
Foo.WF_prop_l2 [in SetProofs]
Foo.WF_prop_r1 [in SetProofs]
Foo.WF_prop_l1 [in SetProofs]
Foo.WF_singleton [in SetProofs]
Foo.WF_validsize [in SetProofs]
Foo.WF_ordered [in SetProofs]
Foo.WF_balanced [in SetProofs]
Foo.WF_size_pos [in SetProofs]
Foo.WF_size_nonneg [in SetProofs]
Foo.WF_size_children [in SetProofs]
Foo.WF_children [in SetProofs]
H
halfRange_smaller [in IntSetProofs]halfRange_isSubrange_testbit [in IntSetProofs]
halfRange_inRange_testbit [in IntSetProofs]
halves_disj [in IntSetProofs]
halves_disj_aux [in IntSetProofs]
halves_disj_aux_aux [in IntSetProofs]
I
inRange_both_not_disj [in IntSetProofs]inRange_both_smaller_subRange [in IntSetProofs]
inRange_isSubrange_false [in IntSetProofs]
inRange_isSubrange_true [in IntSetProofs]
insertBM_Desc [in IntSetProofs]
insert_WF [in IntSetProofs]
insert_Sem [in IntSetProofs]
insert_Nil_Desc [in IntSetProofs]
insert_Desc [in IntSetProofs]
intersection_WF [in IntSetProofs]
intersection_Sem [in IntSetProofs]
intersection_eq [in IntSetProofs]
Int_is_Z [in SetProofs]
Int_eq_is_Z_eq [in SetProofs]
Int_ge_is_Z_ge [in SetProofs]
Int_gt_is_Z_gt [in SetProofs]
Int_le_is_Z_le [in SetProofs]
Int_lt_is_Z_lt [in SetProofs]
Int_mult_is_Z_mult [in SetProofs]
Int_minus_is_Z_minus [in SetProofs]
Int_plus_is_Z_plus [in SetProofs]
isBitMask_bitmapOf [in IntSetProofs]
isBitMask_lor [in IntSetProofs]
isBitMask_testbit [in IntSetProofs]
isBitMask_isBitMask0 [in IntSetProofs]
isBitMask0_lxor [in IntSetProofs]
isBitMask0_land [in IntSetProofs]
isBitMask0_zero_or_isBitMask [in IntSetProofs]
isSubrange_commonRange [in IntSetProofs]
isSubrange_commonRange_r' [in IntSetProofs]
isSubrange_commonRange_l' [in IntSetProofs]
isSubrange_commonRange_l [in IntSetProofs]
isSubrange_commonRange_r [in IntSetProofs]
isSubrange_halfRange_commonRangeDisj [in IntSetProofs]
isSubrange_halfRange [in IntSetProofs]
isSubrange_disj_disj_l [in IntSetProofs]
isSubrange_disj_disj_r [in IntSetProofs]
isSubrange_antisym [in IntSetProofs]
isSubrange_trans [in IntSetProofs]
isSubrange_refl [in IntSetProofs]
isTipPrefix_shiftl_shiftr [in IntSetProofs]
isTipPrefix_prefixOf [in IntSetProofs]
isTipPrefix_prefixMask [in IntSetProofs]
isTipPrefix_suffixMask [in IntSetProofs]
L
land_shiftl_ones [in IntSetProofs]land_pow2_eq [in IntSetProofs]
link_Desc [in IntSetProofs]
log2_le_lin' [in IntSetProofs]
log2_ones [in IntSetProofs]
lor_ones_ones [in IntSetProofs]
lxor_pos [in IntSetProofs]
M
mask_spec [in IntSetProofs]mask_to_upper_bits [in IntSetProofs]
member_Sem [in IntSetProofs]
member_Desc0 [in IntSetProofs]
member_Desc [in IntSetProofs]
msDiffBit_pos [in IntSetProofs]
msDiffBit_larger_r [in IntSetProofs]
msDiffBit_larger_l [in IntSetProofs]
msDiffBit_larger [in IntSetProofs]
msDiffBit_larger_tmp [in IntSetProofs]
msDiffBit_less [in IntSetProofs]
msDiffBit_shiftr_same [in IntSetProofs]
msDiffBit_Same [in IntSetProofs]
msDiffBit_Different [in IntSetProofs]
msDiffBit_sym [in IntSetProofs]
N
nomatch_zero_smaller [in IntSetProofs]nomatch_zero [in IntSetProofs]
nomatch_spec [in IntSetProofs]
N_land_pow2_testbit [in IntSetProofs]
N_pow_pos_nonneg [in IntSetProofs]
N_lt_pow2_testbits [in IntSetProofs]
N_gt_0_neq [in IntSetProofs]
O
of_N_shiftl [in IntSetProofs]of_N_log2 [in IntSetProofs]
ones_spec [in IntSetProofs]
ones_nonneg [in IntSetProofs]
option_int_eq [in SetProofs]
option_int_eqP [in SetProofs]
outside_commonRangeDisj_r [in IntSetProofs]
outside_commonRangeDisj_l [in IntSetProofs]
P
pos_pos [in IntSetProofs]pos_nonneg [in IntSetProofs]
prefixOf_eqb_spec [in IntSetProofs]
prefixOf_eq_shiftr [in IntSetProofs]
prefixOf_nonneg [in IntSetProofs]
R
rangeDisjoint_inRange_false [in IntSetProofs]rangeDisjoint_sym [in IntSetProofs]
rBits_halfRange [in IntSetProofs]
rNonneg_halfRange [in IntSetProofs]
rNonneg_subrange [in IntSetProofs]
rPrefix_shiftr [in IntSetProofs]
rPrefix_inRange [in IntSetProofs]
rPrefix_rBits_range_eq [in IntSetProofs]
S
Sem_change_f [in IntSetProofs]shiftr_eq_ldiff [in IntSetProofs]
shorter_spec [in IntSetProofs]
singleton_WF [in IntSetProofs]
singleton_Sem [in IntSetProofs]
singleton_Desc [in IntSetProofs]
smaller_subRange_other_half [in IntSetProofs]
smaller_not_subrange_disjoint_iff [in IntSetProofs]
smaller_not_subrange_disjoint [in IntSetProofs]
smaller_inRange_iff_subRange [in IntSetProofs]
subRange_smaller [in IntSetProofs]
succ_nonneg [in IntSetProofs]
suffixOf_noneg [in IntSetProofs]
suffixOf_lt_WIDTH [in IntSetProofs]
T
testbit_halfRange [in IntSetProofs]testbit_halfRange_false_false [in IntSetProofs]
testbit_halfRange_isSubrange [in IntSetProofs]
testbit_halfRange_true [in IntSetProofs]
testbit_halfRange_true_false [in IntSetProofs]
testbit_halfRange_false [in IntSetProofs]
testbit_1 [in IntSetProofs]
tip_Desc0 [in IntSetProofs]
to_N_log2 [in IntSetProofs]
U
union_WF [in IntSetProofs]union_Sem [in IntSetProofs]
union_eq [in IntSetProofs]
Z
zero_spec [in IntSetProofs]Z_gtP [in SetProofs]
Z_ltP [in SetProofs]
Z_eqP [in SetProofs]
Z_eq_shiftr_land_ones [in IntSetProofs]
Z_shiftl_injb [in IntSetProofs]
Z_shiftl_inj [in IntSetProofs]
Constructor Index
D
DescBin [in IntSetProofs]DescSem [in IntSetProofs]
DescTip [in IntSetProofs]
Desc0Nil [in IntSetProofs]
Desc0NotNil [in IntSetProofs]
S
SemNil [in IntSetProofs]Inductive Index
D
Desc [in IntSetProofs]Desc0 [in IntSetProofs]
S
Sem [in IntSetProofs]Section Index
F
Foo.t [in MapProofs]Foo.Types [in MapProofs]
Foo.Types.Spec [in MapProofs]
I
Int_And_Z [in SetProofs]M
msDiffBit [in IntSetProofs]O
Option_Int [in SetProofs]Z
ZReflect [in SetProofs]Instance Index
F
Foo.Eq_t [in MapProofs]Foo.Eq_t [in SetProofs]
Foo.Ord_t [in MapProofs]
Foo.Ord_t [in SetProofs]
Definition Index
B
bitmapInRange [in IntSetProofs]C
commonRange [in IntSetProofs]commonRangeDisj [in IntSetProofs]
F
Foo.add [in MapProofs]Foo.add [in SetProofs]
Foo.add [in IntSetProofs]
Foo.add_3 [in MapProofs]
Foo.add_2 [in MapProofs]
Foo.add_1 [in MapProofs]
Foo.before_ordered [in SetProofs]
Foo.before_balancedR [in SetProofs]
Foo.before_balancedL [in SetProofs]
Foo.cardinal [in MapProofs]
Foo.cardinal [in SetProofs]
Foo.cardinal [in IntSetProofs]
Foo.cardinal_1 [in MapProofs]
Foo.choose [in SetProofs]
Foo.choose [in IntSetProofs]
Foo.compare [in SetProofs]
Foo.diff [in SetProofs]
Foo.diff [in IntSetProofs]
Foo.elements [in MapProofs]
Foo.elements [in SetProofs]
Foo.elements [in IntSetProofs]
Foo.elements_3w [in MapProofs]
Foo.elements_2 [in MapProofs]
Foo.elements_1 [in MapProofs]
Foo.elt [in SetProofs]
Foo.elt [in IntSetProofs]
Foo.Empty [in MapProofs]
Foo.empty [in MapProofs]
Foo.empty [in SetProofs]
Foo.Empty [in SetProofs]
Foo.empty [in IntSetProofs]
Foo.Empty [in IntSetProofs]
Foo.empty_1 [in MapProofs]
Foo.eq [in SetProofs]
Foo.eq [in IntSetProofs]
Foo.Equal [in MapProofs]
Foo.equal [in MapProofs]
Foo.equal [in SetProofs]
Foo.Equal [in SetProofs]
Foo.equal [in IntSetProofs]
Foo.Equal [in IntSetProofs]
Foo.equal_2 [in MapProofs]
Foo.equal_1 [in MapProofs]
Foo.Equal_set [in SetProofs]
Foo.Equal_set [in IntSetProofs]
Foo.Equiv [in MapProofs]
Foo.Equivb [in MapProofs]
Foo.eq_key_elt [in MapProofs]
Foo.eq_key [in MapProofs]
Foo.eq_dec [in SetProofs]
Foo.eq_set [in SetProofs]
Foo.eq_dec [in IntSetProofs]
Foo.eq_set [in IntSetProofs]
Foo.Exists [in SetProofs]
Foo.Exists [in IntSetProofs]
Foo.exists_ [in SetProofs]
Foo.exists_ [in IntSetProofs]
Foo.filter [in SetProofs]
Foo.filter [in IntSetProofs]
Foo.find [in MapProofs]
Foo.find_2 [in MapProofs]
Foo.find_1 [in MapProofs]
Foo.fold [in MapProofs]
Foo.fold [in SetProofs]
Foo.fold [in IntSetProofs]
Foo.fold_1 [in MapProofs]
Foo.for_all [in SetProofs]
Foo.For_all [in SetProofs]
Foo.for_all [in IntSetProofs]
Foo.For_all [in IntSetProofs]
Foo.In [in MapProofs]
Foo.In [in SetProofs]
Foo.In [in IntSetProofs]
Foo.inter [in SetProofs]
Foo.inter [in IntSetProofs]
Foo.In_set [in SetProofs]
Foo.In_set [in IntSetProofs]
Foo.is_empty_2 [in MapProofs]
Foo.is_empty_1 [in MapProofs]
Foo.is_empty [in MapProofs]
Foo.is_empty [in SetProofs]
Foo.is_empty [in IntSetProofs]
Foo.key [in MapProofs]
Foo.local_realsize [in SetProofs]
Foo.local_bounded [in SetProofs]
Foo.map [in MapProofs]
Foo.mapi [in MapProofs]
Foo.mapi_2 [in MapProofs]
Foo.mapi_1 [in MapProofs]
Foo.MapsTo [in MapProofs]
Foo.MapsTo_1 [in MapProofs]
Foo.map_2 [in MapProofs]
Foo.map_1 [in MapProofs]
Foo.map2 [in MapProofs]
Foo.map2_2 [in MapProofs]
Foo.map2_1 [in MapProofs]
Foo.mem [in MapProofs]
Foo.mem [in SetProofs]
Foo.mem [in IntSetProofs]
Foo.mem_2 [in MapProofs]
Foo.mem_1 [in MapProofs]
Foo.pack [in MapProofs]
Foo.pack [in SetProofs]
Foo.pack [in IntSetProofs]
Foo.partial_gt [in SetProofs]
Foo.partial_lt [in SetProofs]
Foo.partition [in SetProofs]
Foo.partition [in IntSetProofs]
Foo.remove [in MapProofs]
Foo.remove [in SetProofs]
Foo.remove [in IntSetProofs]
Foo.remove_3 [in MapProofs]
Foo.remove_2 [in MapProofs]
Foo.remove_1 [in MapProofs]
Foo.singleton [in SetProofs]
Foo.singleton [in IntSetProofs]
Foo.subset [in SetProofs]
Foo.Subset [in SetProofs]
Foo.subset [in IntSetProofs]
Foo.Subset [in IntSetProofs]
Foo.t [in MapProofs]
Foo.t [in SetProofs]
Foo.t [in IntSetProofs]
Foo.union [in SetProofs]
Foo.union [in IntSetProofs]
Foo.WF [in MapProofs]
Foo.WF [in SetProofs]
H
halfRange [in IntSetProofs]I
inRange [in IntSetProofs]intersection_Desc [in IntSetProofs]
intersection_body [in IntSetProofs]
isBitMask [in IntSetProofs]
isBitMask0 [in IntSetProofs]
isSubrange [in IntSetProofs]
isTipPrefix [in IntSetProofs]
M
msDiffBit [in IntSetProofs]R
range [in IntSetProofs]rangeDisjoint [in IntSetProofs]
rBits [in IntSetProofs]
rMask [in IntSetProofs]
rNonneg [in IntSetProofs]
rPrefix [in IntSetProofs]
T
tip_widthZ [in IntSetProofs]tip_width [in IntSetProofs]
U
union_Desc [in IntSetProofs]union_body [in IntSetProofs]
W
WF [in IntSetProofs]WIDTH [in IntSetProofs]
| 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 | (536 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 | (2 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 | (5 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 | (24 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 | (3 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 | (1 entry) |
| 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 | (330 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 | (6 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 | (3 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 | (7 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 | (4 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 | (151 entries) |
This page has been generated by coqdoc


Click anywhere in the grid below and drag while holding the mouse button to draw a line.
Undo
Redo
Erase Everything
Show Coordinate Pairs
(0, 0)
JavaScript required.


{{addrInfo.addrLine1}} {{addrInfo.addrLine2}} {{addrInfo.addrLine3}}
addr: {{addrInfo._id}}
result: {{addrInfo.canvassResult}}


Almost all of the complexity in MPI client/server routines addresses the question ``how does the client find out how to contact the server?'' The difficulty, of course, is that there is no existing communication channel between them, yet they must somehow agree on a rendezvous point where they will establish communication. 2.2 Agreeing on a rendezvous point always involves a third party. The third party may itself provide the rendezvous point or may communicate rendezvous information from server to client. Complicating matters might be the fact that a client doesn't really care what server it contacts, only that it be able to get in touch with one that can handle its request.
Ideally, MPI can accommodate a wide variety of run-time systems while retaining the ability to write simple portable code. The following should be compatible with MPI:
A port_name is a system-supplied string that encodes a low-level network address at which a server can be contacted. Typically this is an IP address and a port number, but an implementation is free to use any protocol. The server establishes a port_name with the MPI_OPEN_PORT routine. It accepts a connection to a given port with MPI_COMM_ACCEPT. A client uses port_name to connect to the server.
By itself, the port_name mechanism is completely portable, but it may be clumsy to use because of the necessity to communicate port_name to the client. It would be more convenient if a server could specify that it be known by an application-supplied service_name so that the client could connect to that service_name without knowing the port_name.
An MPI implementation may allow the server to publish a ( port_name, service_name) pair with MPI_PUBLISH_NAME and the client to retrieve the port name from the service name with MPI_LOOKUP_NAME. This allows three levels of portability, with increasing levels of functionality.


| Home | Trees | Indices | Help |
|---|
|
|
object --+ | s_coordinate
return an object that can be indexed to return depths
| Instance Methods | |||
|
|||
|
| Properties | |
| Cs | |
| sc |
| Method Details |
|
| Property Details |
Cs
|
sc
|
| Home | Trees | Indices | Help |
|---|
| Generated by Epydoc 3.0.1 on Mon Apr 20 11:56:30 2009 | http://epydoc.sourceforge.net |


Advanced Usage ¶
In this chapter we will cover some techniques and options that you can use to improve your testing experience and keep your project better organized.
Cest Classes ¶
If you want to get a class-like structure for your Cepts, you can use the Cest format instead of plain PHP. It is very simple and is fully compatible with Cept scenarios. It means that if you feel that your test is long enough and you want to split it, you can easily move it into classes.
You can create a Cest file by running the command:
$ php vendor/bin/codecept generate:cest suitename CestName
The generated file will look like this:
<?php
class BasicCest
{
public function _before(\AcceptanceTester $I)
{
}
public function _after(\AcceptanceTester $I)
{
}
// tests
public function tryToTest(\AcceptanceTester $I)
{
}
}
Each public method of Cest (except those starting with _
) will be executed as a test
and will receive an instance of the Actor class as the first parameter and the $scenario
variable as the second one.
In _before
and _after
methods you can use common setups and teardowns for the tests in the class.
As you see, we are passing the Actor object into tryToTest
method. This allows us to write scenarios the way we did before:
<?php
class BasicCest
{
// test
public function tryToTest(\AcceptanceTester $I)
{
$I->amOnPage('/');
$I->click('Login');
$I->fillField('username', 'john');
$I->fillField('password', 'coltrane');
$I->click('Enter');
$I->see('Hello, John');
$I->seeInCurrentUrl('/account');
}
}
As you see, Cest classes have no parents.
This is done intentionally. It allows you to extend your classes with common behaviors and workarounds
that may be used in child classes. But don't forget to make these methods protected
so they won't be executed as tests.
Cest format also can contain hooks based on test results:
_failed
will be executed on failed test_passed
will be executed on passed test
<?php
public function _failed(\AcceptanceTester $I)
{
// will be executed on test failure
}
public function _passed(\AcceptanceTester $I)
{
// will be executed when test is successful
}
Dependency Injection ¶
Codeception supports simple dependency injection for Cest and \Codeception\TestCase\Test classes.
It means that you can specify which classes you need as parameters of the special _inject()
method,
and Codeception will automatically create the respective objects and invoke this method,
passing all dependencies as arguments. This may be useful when working with Helpers. Here's an example for Cest:
<?php
class SignUpCest
{
/**
* @var Helper\SignUp
*/
protected $signUp;
/**
* @var Helper\NavBarHelper
*/
protected $navBar;
protected function _inject(\Helper\SignUp $signUp, \Helper\NavBar $navBar)
{
$this->signUp = $signUp;
$this->navBar = $navBar;
}
public function signUp(\AcceptanceTester $I)
{
$this->navBar->click('Sign up');
$this->signUp->register([
'first_name' => 'Joe',
'last_name' => 'Jones',
'email' =><EMAIL_ADDRESS>'password' => '1234',
'password_confirmation' => '1234'
]);
}
}
And for Test classes:
<?php
class MathTest extends \Codeception\TestCase\Test
{
/**
* @var \UnitTester
*/
protected $tester;
/**
* @var Helper\Math
*/
protected $math;
protected function _inject(\Helper\Math $math)
{
$this->math = $math;
}
public function testAll()
{
$this->assertEquals(3, $this->math->add(1, 2));
$this->assertEquals(1, $this->math->subtract(3, 2));
}
}
However, Dependency Injection is not limited to this. It allows you to inject any class, which can be constructed with arguments known to Codeception.
In order to make auto-wiring work, you will need to implement the _inject()
method with the list of desired arguments.
It is important to specify the type of arguments, so Codeception can guess which objects are expected to be received.
The _inject()
will only be invoked once, just after creation of the TestCase object (either Cest or Test).
Dependency Injection will also work in a similar manner for Helper and Actor classes.
Each test of a Cest class can declare its own dependencies and receive them from method arguments:
<?php
class UserCest
{
function updateUser(\Helper\User $u, \AcceptanceTester $I, \Page\User $userPage)
{
$user = $u->createDummyUser();
$userPage->login($user->getName(), $user->getPassword());
$userPage->updateProfile(['name' => 'Bill']);
$I->see('Profile was saved');
$I->see('Profile of Bill','h1');
}
}
Moreover, Codeception can resolve dependencies recursively (when A
depends on B
, and B
depends on C
etc.)
and handle parameters of primitive types with default values (like $param = 'default'
).
Of course, you are not allowed to have cyclic dependencies.
Example Annotation ¶
What if you want to execute the same test scenario with different data? In this case you can inject examples
as \Codeception\Example
instances.
Data is defined via the @example
annotation, using JSON or Doctrine-style notation (limited to a single line). Doctrine-style:
<?php
class EndpointCest
{
/**
* @example ["/api/", 200]
* @example ["/api/protected", 401]
* @example ["/api/not-found-url", 404]
* @example ["/api/faulty", 500]
*/
public function checkEndpoints(ApiTester $I, \Codeception\Example $example)
{
$I->sendGET($example[0]);
$I->seeResponseCodeIs($example[1]);
}
}
JSON:
<?php
class PageCest
{
/**
* @example { "url": "/", "title": "Welcome" }
* @example { "url": "/info", "title": "Info" }
* @example { "url": "/about", "title": "About Us" }
* @example { "url": "/contact", "title": "Contact Us" }
*/
public function staticPages(AcceptanceTester $I, \Codeception\Example $example)
{
$I->amOnPage($example['url']);
$I->see($example['title'], 'h1');
$I->seeInTitle($example['title']);
}
}
Key-value data in Doctrine-style annotation syntax:
<?php
class PageCest
{
/**
* @example(url="/", title="Welcome")
* @example(url="/info", title="Info")
* @example(url="/about", title="About Us")
* @example(url="/contact", title="Contact Us")
*/
public function staticPages(AcceptanceTester $I, \Codeception\Example $example)
{
$I->amOnPage($example['url']);
$I->see($example['title'], 'h1');
$I->seeInTitle($example['title']);
}
}
DataProvider Annotations ¶
You can also use the @dataProvider
annotation for creating dynamic examples for Cest classes, using a protected method for providing example data:
<?php
class PageCest
{
/**
* @dataProvider pageProvider
*/
public function staticPages(AcceptanceTester $I, \Codeception\Example $example)
{
$I->amOnPage($example['url']);
$I->see($example['title'], 'h1');
$I->seeInTitle($example['title']);
}
/**
* @return array
*/
protected function pageProvider() // alternatively, if you want the function to be public, be sure to prefix it with `_`
{
return [
['url'=>"/", 'title'=>"Welcome"],
['url'=>"/info", 'title'=>"Info"],
['url'=>"/about", 'title'=>"About Us"],
['url'=>"/contact", 'title'=>"Contact Us"]
];
}
}
@dataprovider
annotation is also available for unit tests, in this case the data provider method must be public.
For more details about how to use data provider for unit tests, please refer to PHPUnit documentation.
Before/After Annotations ¶
You can control execution flow with @before
and @after
annotations. You may move common actions
into protected (non-test) methods and invoke them before or after the test method by putting them into annotations.
It is possible to invoke several methods by using more than one @before
or @after
annotation.
Methods are invoked in order from top to bottom.
<?php
class ModeratorCest {
protected function login(AcceptanceTester $I)
{
$I->amOnPage('/login');
$I->fillField('Username', 'miles');
$I->fillField('Password', 'davis');
$I->click('Login');
}
/**
* @before login
*/
public function banUser(AcceptanceTester $I)
{
$I->amOnPage('/users/charlie-parker');
$I->see('Ban', '.button');
$I->click('Ban');
}
/**
* @before login
* @before cleanup
* @after logout
* @after close
*/
public function addUser(AcceptanceTester $I)
{
$I->amOnPage('/users/charlie-parker');
$I->see('Ban', '.button');
$I->click('Ban');
}
}
Environments ¶
For cases where you need to run tests with different configurations you can define different config environments. The most typical use cases are running acceptance tests in different browsers, or running database tests using different database engines.
Let's demonstrate the usage of environments for the browsers case.
We need to add some new lines to acceptance.suite.yml
:
actor: AcceptanceTester
modules:
enabled:
- WebDriver
- \Helper\Acceptance
config:
WebDriver:
url: 'http://<IP_ADDRESS>:8000/'
browser: 'firefox'
env:
phantom:
modules:
config:
WebDriver:
browser: 'phantomjs'
chrome:
modules:
config:
WebDriver:
browser: 'chrome'
firefox:
# nothing changed
Basically you can define different environments inside the env
root, name them (phantom
, chrome
etc.),
and then redefine any configuration parameters that were set before.
You can also define environments in separate configuration files placed in the directory specified by the envs
option in
the paths
configuration:
paths:
envs: tests/_envs
The names of these files are used as environments names
(e.g. chrome.yml
or chrome.dist.yml
for an environment named chrome
).
You can generate a new file with this environment configuration by using the generate:environment
command:
$ php vendor/bin/codecept g:env chrome
In that file you can specify just the options you wish to override:
modules:
config:
WebDriver:
browser: 'chrome'
The environment configuration files are merged into the main configuration before the suite configuration is merged.
You can easily switch between those configs by running tests with --env
option.
To run the tests only for PhantomJS you just need to pass --env phantom
as an option:
$ php vendor/bin/codecept run acceptance --env phantom
To run the tests in all 3 browsers, list all the environments:
$ php vendor/bin/codecept run acceptance --env phantom --env chrome --env firefox
The tests will be executed 3 times, each time in a different browser.
It's also possible to merge multiple environments into a single configuration by separating them with a comma:
$ php vendor/bin/codecept run acceptance --env dev,phantom --env dev,chrome --env dev,firefox
The configuration is merged in the order given. This way you can easily create multiple combinations of your environment configurations.
Depending on the environment, you may choose which tests are to be executed. For example, you might need some tests to be executed in Firefox only, and some tests in Chrome only.
The desired environments can be specified with the @env
annotation for tests in Test and Cest formats:
<?php
class UserCest
{
/**
* This test will be executed only in 'firefox' and 'phantom' environments
*
* @env firefox
* @env phantom
*/
public function webkitOnlyTest(AcceptanceTester $I)
{
// I do something
}
}
For Cept you should use simple comments:
<?php
// @env firefox
// @env phantom
This way you can easily control which tests will be executed for each environment.
Current values ¶
Sometimes you may need to change the test behavior in real time.
For instance, the behavior of the same test may differ in Firefox and in Chrome.
In runtime we can retrieve the current environment name, test name,
or list of enabled modules by calling the $scenario->current()
method.
<?php
// retrieve current environment
$scenario->current('env');
// list of all enabled modules
$scenario->current('modules');
// test name
$scenario->current('name');
// browser name (if WebDriver module enabled)
$scenario->current('browser');
// capabilities (if WebDriver module enabled)
$scenario->current('capabilities');
You can access \Codeception\Scenario
in the Cept and Cest formats.
In Cept, the $scenario
variable is available by default,
while in Cest you should retrieve it through dependency injection:
<?php
public function myTest(\AcceptanceTester $I, \Codeception\Scenario $scenario)
{
if ($scenario->current('browser') == 'phantomjs') {
// emulate popups for PhantomJS
$I->executeScript('window.alert = function(){return true;}');
}
}
Codeception\Scenario
is also available in Actor classes and StepObjects. You can access it with $this->getScenario()
.
Dependencies ¶
With the @depends
annotation you can specify a test that should be passed before the current one.
If that test fails, the current test will be skipped. You should pass the method name of the test you are relying on.
<?php
class ModeratorCest {
public function login(AcceptanceTester $I)
{
// logs moderator in
}
/**
* @depends login
*/
public function banUser(AcceptanceTester $I)
{
// bans user
}
}
@depends
applies to the Cest
and Codeception\Test\Unit
formats. Dependencies can be set across different classes.
To specify a dependent test from another file you should provide a test signature.
Normally, the test signature matches the className:methodName
format.
But to get the exact test signature just run the test with the --steps
option to see it:
Signature: ModeratorCest:login`
Codeception reorders tests so dependent tests will always be executed before the tests that rely on them.
Shuffle ¶
By default Codeception runs tests in alphabetic order.
To ensure that tests are not depending on each other (unless explicitly declared via @depends
) you can enable shuffle
option.
# inside codeception.yml
settings:
shuffle: true
Alternatively, you may run tests in shuffle without changing the config:
codecept run -o "settings: shuffle: true"
Tests will be randomly reordered on each run. When tests executed in shuffle mode a seed value will be printed. Copy this seed value from output to be able to rerun tests in the same order.
$ codecept run
Codeception PHP Testing Framework v2.4.5
Powered by PHPUnit 5.7.27 by Sebastian Bergmann and contributors.
[Seed]<PHONE_NUMBER>
Pass the copied seed into --seed
option:
codecept run --seed<PHONE_NUMBER>
Interactive Console ¶
The interactive console was added to try Codeception commands before executing them inside a test.
You can run the console with the following command:
$ php vendor/bin/codecept console suitename
Now you can execute all the commands of an appropriate Actor class and see the results immediately.
This is especially useful when used with the WebDriver
module. It always takes too long to launch Selenium
and the browser for tests. But with the console you can try different selectors, and different commands,
and then write a test that should pass when executed.
And a special hint: show your boss how you can easily manipulate web pages with the console and Selenium. It will be easy to convince them to automate this step and introduce acceptance testing to the project.
Running from different folders ¶
If you have several projects with Codeception tests, you can use a single codecept
file to run all of your tests.
You can pass the -c
option to any Codeception command (except bootstrap
), to execute Codeception in another directory:
$ php vendor/bin/codecept run -c ~/projects/ecommerce/
$ php vendor/bin/codecept run -c ~/projects/drupal/
$ php vendor/bin/codecept generate:cept acceptance CreateArticle -c ~/projects/drupal/
To create a project in directory different from the current one, just provide its path as a parameter:
$ php vendor/bin/codecept bootstrap ~/projects/drupal/
Also, the -c
option allows you to specify another config file to be used.
Thus, you can have several codeception.yml
files for your test suite (e.g. to to specify different environments
and settings). Just pass the .yml
filename as the -c
parameter to execute tests with specific config settings.
 You can run tests from a specific directory:
$ php vendor/bin/codecept run tests/acceptance/admin
You can execute one (or several) specific groups of tests:
$ php vendor/bin/codecept run -g admin -g editor
The concept of groups was taken from PHPUnit and behave in the same way.
For Test and Cest files you can use the @group
annotation to add a test to a group.
<?php
/**
* @group admin
*/
public function testAdminUser()
{
}
For Cept files, use pseudo-annotations in comments:
<?php
// @group admin
// @group editor
$I = new AcceptanceTester($scenario);
$I->wantToTest('admin area');
For .feature
-files (Gherkin) use tags:
@admin @editor
Feature: Admin area
Group Files ¶
Groups can be defined in global or suite configuration files. Tests for groups can be specified as an array of file names or directories containing them:
groups:
# add 2 tests to db group
db: [tests/unit/PersistTest.php, tests/unit/DataTest.php]
# add all tests from a directory to api group
api: [tests/functional/api]
A list of tests for the group can be passed from a Group file. It should be defined in plain text with test names on separate lines:
tests/unit/DbTest.php
tests/unit/UserTest.php:create
tests/unit/UserTest.php:update
A group file can be included by its relative filename:
groups:
# requiring a group file
slow: tests/_data/slow.txt
You can create group files manually or generate them from third party applications. For example, you can write a script that updates the slow group by taking the slowest tests from xml report.
You can even specify patterns for loading multiple group files with a single definition:
groups:
p*: tests/_data/p*
This will load all found p*
files in tests/_data
as groups. Group names will be as follows p1,p2,...,pN.
Formats ¶
In addition to the standard test formats (Cept, Cest, Unit, Gherkin) you can implement your own format classes to customise your test execution. Specify these in your suite configuration:
formats:
- \My\Namespace\MyFormat
Then define a class which implements the LoaderInterface
namespace My\Namespace;
class MyFormat implements \Codeception\Test\Loader\LoaderInterface
{
protected $tests;
protected $settings;
public function __construct($settings = [])
{
//These are the suite settings
$this->settings = $settings;
}
public function loadTests($filename)
{
//Load file and create tests
}
public function getTests()
{
return $this->tests;
}
public function getPattern()
{
return '~Myformat\.php$~';
}
}
Shell auto-completion ¶
For bash and zsh shells, you can use auto-completion for your Codeception projects by executing the following in your shell (or add it to your .bashrc/.zshrc):
`
bash
BASH ~4.x, ZSH ¶
source <([codecept location] _completion --generate-hook --program codecept --use-vendor-bin)
BASH ~3.x, ZSH ¶
[codecept location] _completion --generate-hook --program codecept --use-vendor-bin | source /dev/stdin
BASH (any version) ¶
eval $([codecept location] _completion --generate-hook --program codecept --use-vendor-bin)
`
Explanation ¶
By using the above code in your shell, Codeception will try to autocomplete the following:
- Commands
- Suites
- Test paths
Usage of -use-vendor-bin
is optional. This option will work for most Codeception projects, where Codeception is located in your vendor/bin
folder.
But in case you are using a global Codeception installation for example, you wouldn't use this option.
Note that with the -use-vendor-bin
option, your commands will be completed using the Codeception binary located in your project's root.
Without the option, it will use whatever Codeception binary you originally used to generate the completion script ('codecept location' in the above examples)
Conclusion ¶
Codeception is a framework which may look simple at first glance but it allows you to build powerful tests with a single API, refactor them, and write them faster using the interactive console. Codeception tests can be easily organized in groups or Cest classes.


Hi folks,
I'm Mo from Stuttgart. I like startups, cycling, fitness, travelling, reading and gadgets.
#Entrepreneur
I've started several apps and ideas with moderate success but learned a lot during that time. Now I am very active with a solution for the waste management industry.
#Athlete
As a former german champion in cycling in junior class I definitely need to work out regularly to achieve a healthy balance.
#Lecturer
I regularly host lectures about entrepreneurship and technology at universities.
If you have questions, suggestions, criticism or just want to have a cup of coffee or a glass of wine with me please do not hesitate to contact me.
Social


_______________________________________________________________________________________________
Today we’ll cover statistical concepts and tests commonly used in cancer research. The dataset we’ll access is a subset of the ALL expression data whose patient information we worked with in the ﬁrst day’s material. In addition to that information we’ll access 1000 associated expression microarray features that present the highest variance across the patient samples. The data have been saved in a binary format to reduce ﬁle sizes.
_______________________________________________________________________________________________
Let’s look a little more closely at patient information in the info ﬁle:
∙ Some simple plots of patient ages – note the nested functions!
∙Exercise: Plot the sortedAge with markers at each data point and connect the points with red lines.
∙Exercise: Plot one variable (e.g., age) as a function of another (e.g., sex).  Hint: review the ’doc’ data frame from last week’s lesson for column descriptions.
_______________________________________________________________________________________________
Use plot to visualize the distribution of female and male ages in the info data set.
It looks like females are on average older than males. Use t.test to ﬁnd out.
Check out the help page for t.test
What are all those additional arguments to t.test? For example, what is the meaning of the var.equal argument?Why are there 79.88 degrees of freedom?
A t-test can also be viewed as an analysis of variance (ANOVA); analysis of variance is a form of linear model. Use lm to ﬁt a linear model that describes how age changes with sex; the anova function summarizes the linear model in a perhaps more familiar ANOVA table.
What kinds of assumptions are being made in the linear model, e.g., about equality of variances? Try plotting fit; what are the ﬁgures trying to tell you?
fit is an example of an R object. Find out it’s class
plot is an example of an R generic; it has diﬀerent methods implemented for diﬀerent classes of objects. Use methods to see available methods
Look up the help page for the plot generic, lm method with
Fitted models can be used in other functions, for instance to predict values for new data.  Consult the help page for the predict.lm method, and calculate the expected value of the ﬁtted model for males and for females.
What do the predicted values correspond to in the t.test? Use coefficients to extract the coeﬃcients of the ﬁtted model.
Interpret the (Intercept) and sexM coeﬃcients in terms of female and male ages.
The article from which the info object is derived states that “Although chromosome translocations and molecular rearrangements are relatively infrequent in T-lineage ALL, these events occur commonly in B-lineage ALL and reﬂect distinct mechanisms of transformation”. Let’s investigate this statement.
The relevant columns of data are summarized as
Simplify the number of BT levels by creating a map between subtypes and types
The names of the map are the subtypes, the elements are the types. Map the levels of the BT variable from sub-type to type with the following command, and cross-tabulate the data
The data are qualitatively consistent with the statement that molecular rearrangements are more common in B-lineage ALL. Let’s test this with a chi-squared test
Interpret the results. What about additional parameters documented on ?chisq.test?
_______________________________________________________________________________________________
Earlier we read in the ALL1k object. This is a data frame. The rows represent 1000 microarray probe sets. The ﬁrst two columns contain information about the probe sets. The remaining 128 columns are (normalized) expression values of 128 samples. The 128 samples correspond to the phenotypic data in the info object we’ve been working with. The following lines take the expression values and transform them from a data.frame to a matrix, adjusting the row and column names to reﬂect the probe and sample ids.
Some of the results below involve plots, and it’s convenient to choose pretty and functional colors. We use the RColorBrewer package; see colorbrewer.com.
‘divergent’ is a vector of colors that go from red (negative) to blue (positive). ‘higlight’ is a vector of length 2, light and dark green.
It is hard to visualize data from 1000 probesets and 128 samples. In addition, the data suﬀers from the problem that there are many more measurements per sample (1000) than there are samples (128). For these reasons, we might wish to reduce the number of dimensions in which the data is represented. One way of reducing the dimensionality is by calculating principle components. Here we calculate principle components:
The principle components are, roughly, vectors that pass through the data in such a way as to explain as much variability as possible. We can visualize the data in two-dimensional space by plotting the ‘rotation’, coloring points by whether they belong to the B or T ALL lineage (we will discuss other arguments to plot in a subsequent class).
Notice that the B and T lineages separate quite well.
There are a number of variants to principle components, and some tricky statistical issues involved even in the simple example above, so proceed with caution!
Clustering, or ‘unsupervised machine learning’, tries to group samples based on similarity. We start by calculating the correlation between each of our samples.
cm is a 128 x 128 matrix, and it measures the correlation between each pair of samples – samples with similar patterns of gene expression will be correlated.
We can use the strength of correlation as a basis for describing the distance between samples. Two samples will be ‘near’ each other if they have similar patterns of correlation with other samples.
There are several ways of measuring distance; the default is a euclidean measure.
The next step is to group (cluster) samples that are similar to one another into a dendrogram summarizing similarity.
Somewhat more revealing of structure is a heatmap, with rows and columns clustered as we’ve just described, and with a column color bar to indicate whether the sample came from a B or T lineage sample.
The plot shows that, mostly, the B lineage samples cluster together, and the T lineages cluster together. If this were an exploratory analysis, one would look carefully to ensure that the mis-clustered samples were not mis-labeled.
Classiﬁcation (‘supervised machine learning’) groups samples into a pre-speciﬁed number of groups. There are many varieties of classiﬁcation. k-means classiﬁcation aims to place k ‘centroids’ in such a way that the sum of squares of each point to the nearest centroid is minimized. Here we perform k-means classiﬁcation with 2 groups, anticipating that we will recover the B and T ALL lineages; we use set.seed to set the random number seed to a particular (arbitrary) value to ensure reproducibility.
The ‘confusion’ matrix is one measure of how eﬀective the classiﬁcation is; here we see that all but one of the samples were assigned to the correct group.
There are objective criteria for parameter choice and validation of supervised machine learning algorithms.
_______________________________________________________________________________________________
There are several important lessons from this brief tour of statistical functions in R:
_______________________________________________________________________________________________
In the next class we’ll use data from the Center for Disease Control’s Behavioral Risk Factor Surveillance System (BRFSS) annual survey. Check out the web page for a little more information. We are using a small subset of this data, including a random sample of 10000 observations from each of 1990 and 2010. As preparation for the class:
_______________________________________________________________________________________________


Bootstrap Icons
Bootstrap icons are a great way to add small graphics to your site. It's another free library from the makers of Bootstrap. Let's take a look at how it works.
Install
<link rel="stylesheet"<EMAIL_ADDRESS>/>
npm i bootstrap-icons
There's a few different options for installing the icons. You have access to a CDN through this link
You can download the icons, which include some fonts by clicking on this button.
Finally, if you're working with build tools, you can npm install them.
SVG
<svg xmlns="http://www.w3.org/2000/svg" width="16" height="16" fill="currentColor" class="bi bi-emoji-smile" viewBox="0 0 16 16"><path d="M8 15A7 7 0 1 1 8 1a7 7 0 0 1 0 14zm0 1A8 8 0 1 0 8 0a8 8 0 0 0 0 16z"/><path d="M4.285 9.567a.5.5 0 0 1 .683.183A3.498 3.498 0 0 0 8 11.5a3.498 3.498 0 0 0 3.032-<IP_ADDRESS> 0 1 1 .866.5A4.498 4.498 0 0 1 8 12.5a4.498 4.498 0 0 1-3.898-<IP_ADDRESS> 0 0 1 .183-.683zM7 6.5C7 7.328 6.552 8 6 8s-1-.672-1-1.5S5.448 5 6 5s1 .672 1 1.5zm4 0c0 .828-.448 1.5-1 1.5s-1-.672-1-1.5S9.448 5 10 5s1 .672 1 1.5z"/></svg>
- Maximum flexibility
- Classes, size colors
- Edit SVG
- Lots of text
The icons are designed as SVGs, so you can add the SVG code directly into your projects. The advantage here is maximum flexibility.
You can change the size or colors, add classes and edit the code as you would any other SVGs.
To get the code, go to the website and do a search through the icons. Click on an individual element's clipboard icon to copy the HTML code to your clipboard. You also have the option of downloading the code just for that SVG, so you can edit that if you want.
Sprite
<svg class="bi" width="32" height="32" fill="currentColor">
<use xlink:href="bootstrap-icons.svg#emoji-smile" />
</svg>
- Must download
- Less code/smaller
- Problems with chrome
You can also add icons by creating an svg with an element that has a use attribute. This will have a link to where the icon is and that means that this won't work with a CDN.
It's definitely a lot less code and if you're using an icon a lot on the same page, it makes your files smaller because you're using the SVG only once.
However, there are some problems when you use this with chrome accross domains.
Also, notice the way you use this is by calling the same icon and then passing along a hash with the icon name getting rid of some of what you copy.
Icon Fonts

- Easiest
- Less code/smaller
- Styling
- Usability
Icon fonts are a convenient way to use icon files because they allow you to use a simple
tag and use a class to activate the icon.
Like with Sprites, you end up with a lot less code and smaller files since the font is only loaded once.
Notice that the way you style these is by using text-color and that also means that their size is tied to the font size of the current element.
That reminds me. There's a bit of drama and discussion about fonts because technically SVGs are considered superior for usability.
There's one more way to use icons and that's to use a simple image tag with a link to the svg file. It's the least useful way of using these, so I'm not going to cover it.
Practice
- Add an icon using fonts
- Add an icon using SVGs
- Change icon color/size
- Adjust spacing
Let's take a look at how this works. I've got a codepen prepared for you so you can practice.
Note: I've already added bootstrap and bootstrap icons as well as the javascript to this template. Also, my codepen might look at bit different than yours.

Font Icons

<svg xmlns="http://www.w3.org/2000/svg"
overflow="visible" width=".8em" height=".8em"
class="bi bi-heart-fill me-2" viewBox="0 0 16 16">
<path
fill="transparent" stroke="red" fill-rule="evenodd"
d="M8 1.314C12.438-3.248 23.534 4.735 8 15-7.534 4.736 3.562-3.248 8 1.314z"/>
</svg>SVG Icons


The Bokeh server is an optional component that can be used to provide additional capabilities, such as:
The Bokeh server is built on top of Flask, specifically as a
Flask Blueprint. You can embed the Bokeh server functionality inside
a Flask application, or deploy the server in various configurations
(described below), using this blueprint. The Bokeh library also ships
with a standalone executable bokeh-server
that you can easily run to
try out server examples, for prototyping, etc. however it is not intended
for production use.
The basic task of the Bokeh Server is to be a mediator between the original data and plot models created by a user, and the reflected data and plot models in the BokehJS client:
Here you can see illustrated the most useful and compelling of the Bokeh server: full two-way communication between the original code and the BokehJS plot. Plots are published by sending them to the server. The data for the plot can be updated on the server, and the client will respond and update the plot. Users can interact with the plot through tools and widgets in the browser, then the results of these interactions can be pulled back to the original code to inform some further query or analysis (possibly resulting in updates pushed back the plot).
We will explore the capabilities afforded by the Bokeh server in detail below.
The core architecture of bokeh-server
develops around 2 core models:
Document
User
A User controls authentication information at the user level and both models
combined determines the authorization information regarding user documents
that are private, so can be accessed only by the user, or public.
One thing to keep in mind when interacting with bokeh-server is that every session open to the server implies that an user is logged in to the server. More information about this can be found at the Authenticating Users paragraph below.
If Bokeh was installed running python setup.py or using a conda package, then the
bokeh-server
command should be available and you can run it from any directory.
bokeh-server
Note
This will create temporary files in the directory in which you are running it.
You may want to create a ~/bokehtemp/
directory or some such, and run the
command there
If you have Bokeh installed for development mode (see Building and Installing), then you should go into the checked-out source directory and run:
python ./bokeh-server
Note
bokeh-server
accepts many input argument options that let the user customize
it’s configuration. Although we will use a few of those in this section we highly
encourage the user to run bokeh-server -h
for more details.
Now that we have learned how to run the server, it’s time to start using it!
In order to use our running bokeh-server
we need to create a plot and store it
on the server.
It’s possible to do it by using the Document
and the Session
objects.
The former can be considered as a namespace
object that holds the plot
information while the later will take care of connecting and registering the
information on the server. It also acts as an open channel that can be used
to send/receive changes to/from the server.
As usual, the bokeh.plotting
interface provides a set of useful shortcuts
that can be used for this. The result is that creating a line plot as a static
html file is not so different than creating it on a bokeh-server
, as we can
see on the following example:
from bokeh.plotting import figure, output_server, show
output_server("line") # THIS LINE HAS CHANGED!
p = figure(plot_width=400, plot_height=400)
# add a line renderer
p.line([1, 2, 3, 4, 5], [6, 7, 2, 4, 5], line_width=2)
show(p)
As mentioned before bokeh-server
does implement the concept of authentication.
At this point one could raise the following question: Really? So why I wasn’t asked
to login to register or the plot I’ve created in the previous section?
This is a good question and the reason is because bokeh-server
defaults to
single user mode when launched. This is very important to keep in mind: when in
single user mode every request is automatically logged in as a user with username
defaultuser
.
However for teams, and for plot publishing (see Publishing to the Server for
more details), it makes more sense to add an authentication layer. This way
users won’t be able to overwrite each other’s plots. To do enable multi user
mode, you need to turn on the multi_user bokeh server setting by using the
command line parameter -m
. Once this is done, all scripts that use the
bokeh server must authenticate with the bokeh server.
Once again the Session
object can be used to create or login users to the
server.
An user can be created with the following python code:
session = Session(root_url=url)
session.register(username, password)
or login with:
session = Session(root_url=url)
session.login(username, password)
Note
~/.bokeh
directory), so logging in is not necessary in subsequent
invocations.As mentioned earlier, when running in multi user mode, a plot must be published so that different logged users can access it. This can be done, again, using the session object as the following snippet shows:
output_server('myplot')
# make some plots
cursession().publish()
A public link to a plot on the bokeh server page can be viewed by appending
?public=true
To the url - for example if you have the url to a
plot http://localhost:5006/bokeh/doc/some-doc-id/some-plot-id
,
You can generate a public link to the published plot using
http://localhost:5006/bokeh/doc/some-doc-id/some-plot-id?public=true
.
Note
In addition, the autoload_server function call in bokeh.embed shown in server data also takes a public=true keyword argument, which will generate an embeddable html snippet that will load the public version of a given plot
Streaming data to automatically update plots is very straightforward
using bokeh-server
. As seen previously, Session
object exposes
the session.store_objects
method that can be used to update objects
on the server (and consequently on the browser) from your python code.
Here’s a simple example:
import time
from random import shuffle
from bokeh.plotting import figure, output_server, cursession, show
# prepare output to server
output_server("animated_line")
p = figure(plot_width=400, plot_height=400)
p.line([1, 2, 3, 4, 5], [6, 7, 2, 4, 5], name='ex_line')
show(p)
# create some simple animation..
# first get our figure example data source
renderer = p.select(dict(name="ex_line"))
ds = renderer[0].data_source
while True:
# Update y data of the source object
shuffle(ds.data["y"])
# store the updated source on the server
cursession().store_objects(ds)
time.sleep(0.5)
Notice that in order to update the plot values we only need to update it’s
datasource and store it on the server using the session
object.


-->
Please choose restaurant
search bar placeholder
your order
Food charge:
£ 0.00
Delivery charge:
£ 2.00
Total price:
£ 0.00
Terms and Conditions


HL7V2ExpressionConfiguration
Table of Contents
Description
Use this expression configuration for the Evaluator when parsing HL7V2 files.
When the static constructor is called, the encodingConversions are rebuilt using the current values of the static delimiters, and the specialSegmentHeaders are initialized. The default values are MSH, FHS, and BHS.
Every time Evaluate is called internally on an expression, this expression configuration calls an internal method named Setup that re-initializes the message segment. So each line of the hl7v2 message is an expression that the Evaluator converts into an HL7V2MessageSegment.
Inside of the constructor the operators and options are initialized. The SolveOperatorExpression callback for the AdditionOperator is where the main hl7v2 parsing takes place. It extracts the data from the hl7, applies structure via an HL7V2Field added to an HL7V2MessageSegment. After, it returns a DefaultExpressionResult, which can be found in ExpressionConfigurationBase.
Static Fields
- fieldDelimiter: This separates fields in an hl7v2 message segment.
- componentDelimiter: This separates components within a field repetition in an hl7v2 message segment. This is defined within special segments, such as MSH.
- escapeDelimiter: This is used to encode / decode data within hl7v2 messages. This is defined within special segments, such as MSH.
- subComponentDelimiter: This separates sub components within components in an hl7v2 message segment. This is defined within special segments, such as MSH.
- fieldRepetitionDelimiter: This separates field repetitions within fields in an hl7v2 message segment. This is defined within special segments, such as MSH.
- presentButNull: This string is used to define data that should be treated as null as specified in the hl7 v2 specification.
- specialSegmentHeaders: These segment headers should be treated separately from other segments because they expose the delimiters that the message should use when evaluating the segment.
- encodingConversions: Encoding conversions are used to encode / decode data for hl7 data using the delimiters wrapped around the escape character.
Static Methods
- RebuildEncodingConversions: This rebuilds the encodingConversions so that when EncodeString or DecodeString is called it uses the latest values from the delimiters and escape character. Make sure to call this if you update any of the delimiters or escape characters before calling EncodeString or DecodeString.
- EncodeString: Encodes a string for use in an hl7 v2 message using the delimiters wrapped around the escape character.
- DecodeString: Decodes a string for use in an hl7 v2 message using the delimiters wrapped around the escape character.
Properties
options = new ExpressionConfigurationOptions
{
IgnoreWhitespaceOutsideQuotes = true,
IgnoreParentheses = true,
IgnoreQuotesValidation = true
};
Methods
- GetHL7V2MessageSegment: Returns the message segment. Called internally when evaluating an hl7v2 file to build the hl7v2 message.


Next: string=, Previous: string-upcase, Up: Strings Dictionary
string-trim
character-bag string ⇒ trimmed-string
string-left-trim
character-bag string ⇒ trimmed-string
string-right-trim
character-bag string ⇒ trimmed-string
character-bag—a sequence containing characters.
string—a string designator.
trimmed-string—a string.
string-trim returns a substring of string, with all characters in character-bag stripped off the beginning and end. string-left-trim is similar but strips characters off only the beginning; string-right-trim strips off only the end.
If no characters need to be trimmed from the string, then either string itself or a copy of it may be returned, at the discretion of the implementation.
All of these functions observe the fill pointer.
(string-trim "abc" "abcaakaaakabcaaa") ⇒ "kaaak" (string-trim '(#\Space #\Tab #\Newline) " garbanzo beans ") ⇒ "garbanzo beans" (string-trim " (*)" " ( *three (silly) words* ) ") ⇒ "three (silly) words" (string-left-trim "abc" "labcabcabc") ⇒ "labcabcabc" (string-left-trim " (*)" " ( *three (silly) words* ) ") ⇒ "three (silly) words* ) " (string-right-trim " (*)" " ( *three (silly) words* ) ") ⇒ " ( *three (silly) words"
The implementation.


Risin' High (feat Raashan Ahmad)
Ancient Astronauts • We Are to Answer
The Gun
Lorn • Ask The Dust
The Gun
Lorn • Anvil
I Came Running
Ancient Astronauts • We Are to Answer
Terrain
pg.lost • Key
Vorel
Russian Circles • Guidance
Intro / Sweet Glory
Die Digital • Jimkata
Offcut #6
Little People • We Are But Hunks of Wood Remixes


--- layout: post title: A Perl of Wisdom date: '2013-08-11T21:37:00-07:00' tags: [] tumblr_url: http://blog.dishbreak.com/post/58031258802/a-perl-of-wisdom ---
I’m a perl fan, so here goes a bad joke:
$thought = "Once you learn to use a hammer, everything looks like a nail.";
$thought =~ s/a hammer/Perl/;
$thought =~ s/nail/parsable text file/;


NoSQL Linkedin assessment skills test
Q1. Which types of indexes are available in CosmosDB? 1. range and spatial <<<<<–CORRECT 2. secondary and primary key 3. secondary and spatial 4. range and primary key
Q2. You want to connect a DynamoDB stream to AWS Lambda function? 1. DynamoDB table 2. DynamoDB trigger <<<<<–CORRECT 3. DynamoDB item 4. DynamoDB index
Q3. To index a field that holds an array value in MongoDB, which index type do you create? 1. partial 2. sparse 3. compound 4. multikey <<<<<–CORRECT
Q4. You want to test HBASE on your laptop using the fewest number of steps. What do you do? 1. Set up Hadoop in pseudo-distributed mode. 2. Set up HBASE in local mode. 3. Set up HBASE in pseudo-distributed mode. <<<<<–CORRECT 4. Set up Hadoop in local mode.
Q5. You need to create a document database that supports database triggers. Which NoSQL database should you use? 1. DynamoDB <<<<<–CORRECT 2. BigTable 3. Redis 4. MongoDB
Q6. What is recommended size for Redis keys? 1. medium 2. short <<<<<–CORRECT 3. single bit
4. long
Q7. You need to design security for DynamoDB to allow users read-only access to certain items and attributes in a table. What do you do? 1. Use lAM policy conditions 2. Use lAM roles 3. Use VPC endpoint 4. Use lAM policies <<<<<–CORRECT
Q8. What does redis use to sort the elements of a sorted set? 1. Scores. 2. Ids. 3. Values. 4. Keys. <<<<<–CORRECT
Q9.You need to change the shard key of an existing MongoDB collection. What do you do? 1. Dump the collection data, drop the collection, create a new collection and shard key, import the data. 2. Add second shard key and drop the first shard key. 3. Dump the collection data, drop the collection, presplit the data, create a new collection and shard key, import the data. <<<<<–CORRECT 4. Drop and recreate the shard key.
Q10. Polyglot storage means using multiple types of what in the same application? 1. Security systems. 2. Database systems. 3. Storage systems. 4. Query systems. <<<<<–CORRECT
Q11. You need to implement the simplest possible scalable, in-memory cache for your AWS application. Which service do you select? 1. Elasticache using Memcached. 2. DynamoDB. 3. DynamoDB Accelerator (DAX). 4. Elasticache using Redis. <<<<<–CORRECT
Q12. You are doing data modelling for Google BigTable. Which statement expresses if and when you should split entities across multiple rows? 1. Keep all information for an entity in a single row. Store related entities in adjacent rows.
2. Keep all information for an entity in a single row. 3. Split entities across multiple rows if the entity data is over thousands of MBs, or if it does not need atomic updates and reads. 4. Split entities across multiple rows if the entity data is over hundreds of MBs, or if it does not need atomic updates and reads. <<<<<–CORRECT
Q13. Which two characteristics define Amazon Quantum Ledger Database? 1. Key-value data model; transactionally consistent with ACID semantics.
2. Document data model; transactionally consistent with ACID semantics. <<<<<–CORRECT 3. Key-value data model; transactions with tunable consistency. 4. Document data model; transactions with tunable consistency.
Q14. You need to design the primary key for DynamoDB based on three attributes. What do you do? 1. Designate all three fields as the primary key.
2. Concatenate all three fields into one new field, then designate that new field as the primary key. <<<<<–CORRECT 3. Designate two fields of the three fields as the primary key. 4. Concatenate two fields into one new field, then designate that new field and the remaining field as the primary key.
Q15. You need to design the primary key for DynamoDB based on three attributes. What do you do? 1. Designate all three fields as the primary key.
2. Concatenate all three fields into one new field, then designate that new field as the primary key. <<<<<–CORRECT 3. Designate two fields of the three fields as the primary key. 4. Concatenate two fields into one new field, then designate that new field and the remaining field as the primary key.
Q16. Which of these data types should you avoid in designing a Google Bigtable row key?
- multi-valued identifiers
- string identifiers
- timesstamps
- frequently updated identifiers <<<<----Correct
Q17. Your startup is building a prototype that has an evolving schema. Your data will be eventually consistent. Your application is hosted in AWS. Which databse do you choose?
- Neptune
- DocumentDB
- DynamoDB <<<<----Correct
- Amazon Aurora
Q18. You need to create a scalable databse that allows you to share documents across authorized mobile clients in real time. What Google NoSQL database should you use?
- Memorystore
- Datastore
- Firebase <<<<----Firebase
- Bigtable
Q19. You want to test HBase on your laptop using the fewest number of steps. What do you do?
- Set up HBase in local mode.
- Set up Hadoop in pseudo-distributed mode.
- Set up HBase in pseudo-distributed mode.
- Set up Hadoop in local mode. <<<<----Correct
Q20. You need to design security for DynamoDB to allow users read-obly access to certain items and attriutes in a table. What do you do?
- Use IAM roles.
- Use IAM plicy conditions. <<<<----Correct
- Use a VPC endpoint.
- Use IAM plicies.
Q21. You need to design a primary key for DynamoDb based on three attributes. What do you do?
- Concatenate all three fields into into one new field, than disignate that new field as the primary key.
- Concatenate two fileds into one new field, than disignate that new field and the remaining field as the primary key.
- Designate all three fields as the primary key. <<<<----Correct
- Designate two filds of the three fields as the primary key.
Q22. What does Redis use to sort the elements of a sorted set?
- keys
- values
- scroes <<<<----Correct
- ids
Q23. You need to create a document database that supports database triggers. Which NoSQL database should you use?
- DynamoDb <<<<----Correct
- Redis
- MongoDB
- Bigtable
Q24. You need to implement the simples possible scalable, in-memory cache for your AWS application. Which service do you select?
- DynamoDb Accelerator (DAX) <<<<----Correct
- ElastiCache using memcached
- ElastiCache using Redis
- DynamoDB
Q25. Which statement is prefered Cypher code for Neo4j?
- MATCH (:Person)-->(:Card)-->(:Company) RETURN count(vehicle)
- Match (:Person)-->(:Car):(vehicle:Car)-->(:Company) RETURN count(vehicle)
- MATCH (:Person)-->(vehicle:Car)-->(:Company) RETURN count(vehicle) <<<<----Correct
- MATCH (:Person)-->(:Card), (vehicle:Car)-->(:Company) RETURN count(vehicle)
Q26. You need multi-item ACID transactions with snapshot isolation within a partition for your cloud-based application. Which NoSQL databse do you choose?
- Bigtable
- GraphDB
- DynamoDB
- Cosmos DB <<<<----Correct
Q27. You need to control your application’s batch updates destination for your Bigtable multinode cluster. Which action do you take?
- Create a custom app profile to route batch updates.
- Create a custom app profile to route the batch update from that client.
- Update the default app profile to route the natch update from that client. <<<<--- May be
- Use the default app profile to route batch updates.
Q29. Polyglot storage mean using multiple types of what in the same application?
- security systems
- databse systems
- query systems
- storage systems <<<<----Correct
Q30. Your query to verify that your Redis key is configured to support expiring user information on a efined interval returns -2. What does this value indicate?
- The queried key value expired in the last two secodns.
- The queried key value exists, but has no associated expire value.
- The queried key value does not exist. <<<<----Correct
- There are two expired keys with this value.
Q31. You are designing a MongoDB schema to support queries that will include lookups. What should you do?
- Create an index on the key value used as the primary key.
- Create an index on the key value used as the foreign key.
- Create a multicolumn index on the key value used as the foreign key and the most unique column in the document. <<<<----Correct
- Create a multicolumn index on the key value used as the primary and also the forign key.
Q32. What is the aggregation operator for a join concept in MongoDB?
- $group
- $match
- $lookup <<<<----Correct
- $project
Q33. For your mobile application, you need to select a Google cloud databse that can support compound, filtered document queries. Which do you choose?
- Cloud SQL
- Cloud Spanner
- Cloud Firestore <<<<----Correct
- Cloud Firebase
Q34. To bulk load data into Amazon Neputn, what do you do?
- Upload data to S3 VPC endpoint, Use the Neptun loader to load from s3 into your Neptune instance <<<<----Correct
- Ad data to a Kinesis stream, and use the Neptune loade to load from S# into your Neptun instance.
- Add data to a Kisnesis stream, and create a Kinesis stream VPC endpoint. Use the Nepune loader to load from S3into your Neptune instance.
- Upload data to S3. Use the neptune loader to load from S3 into your Neptune instance.
Q35. You need to create a pub/sub server. Which databse do you use?
- Neo4j
- Cassandra
- Redis <<<<----Correct
- MySQL
Q36. You want to connect a DynamoDb stream to an AWS lamdba function. Which one of these object do you create.
- DynamoDb table
- DynamoDB trigger <<<<----Correct
- DynamoDB item
- DYnamoDB index
Q37. Which two types of indexes are available in Cosmos DB?
- secondery and primary key <<<<----Correct
- secondary and spatial
- range and spatial
- range and primary key
Q38. SQL databses and NoSQL are which types of scalable?
- horizontally, infinitely
- vertically, horizontally <<<<----Correct
- vertically, infinitely
- horizonally, vertically
Q39. You need to create a scalable database that allows you to query data nodes and edges efficiently. What do you use?
- a relational databse
- a columnstore databse
- a document databse
- a graph database <<<<----Correct
Q40. You are developing a model for a graph databse. Your data will be moved from a relatinal databse into Neo4j. Which of these transformations apply?
- Rows become labes: bales become nodes.
- Tables become labels: rows become nodes.
- Tables become collections: rows become items.
- Rows become collections: tables become items. <<<<----May be
Q41. To index a field that holds an array value in MongoDB, which index type do you create?
- sparse
- compound
- partial
- multikey <<<<-----Correct
Q42. You need to execute a command for MongoDB that does NOT load values from the .mongorc.js file. What do you do ?
- Delete the .monorc.js file and restart mongo shell.
- Use the mongo shell to create a command with --norc option
- Rem all lines in the .mongorc.js file ad restart mongo shell.
- Use the mongo shell to create a command with --nodedefault option. <<<<----Not sure
Q43. What is the recommended size for Redis keys?
- long
- short
- medium
- a single bit <<<<----May be