W (definition)
wB [in wB]
weak [in weak]
weak_excluded_middle [in weak_excluded_middle]
weak_generalized_excluded_middle [in weak_generalized_excluded_middle]
well_founded [in well_founded]
WEqPropertiesOn.Add [in Add]
WEqPropertiesOn.sum [in sum]
WEqProperties_fun.Add [in Add]
WEqProperties_fun.sum [in sum]
WF [in WF]
WFactsOn.eqb [in eqb]
WFactsOn.Subset_refl [in Subset_refl]
WFactsOn.Subset_trans [in Subset_trans]
WFacts_fun.eqb [in eqb]
WFacts_fun.eqb [in eqb]
WFacts_fun.option_map [in option_map]
WFacts_fun.compat_cmp [in compat_cmp]
WFacts_fun.Equal_ST [in Equal_ST]
wof [in wof]
WOps.elt [in elt]
word [in word]
WPropertiesOn.Add [in Add]
WPropertiesOn.of_list [in of_list]
WPropertiesOn.to_list [in to_list]
WProperties_fun.transpose_neqkey [in transpose_neqkey]
WProperties_fun.exists_ [in exists_]
WProperties_fun.to_list [in to_list]
WProperties_fun.to_list [in to_list]
WProperties_fun.Add [in Add]
WProperties_fun.Add [in Add]
WProperties_fun.filter_range [in filter_range]
WProperties_fun.partition [in partition]
WProperties_fun.update [in update]
WProperties_fun.Disjoint [in Disjoint]
WProperties_fun.exists_dom [in exists_dom]
WProperties_fun.filter [in filter]
WProperties_fun.of_list [in of_list]
WProperties_fun.of_list [in of_list]
WProperties_fun.for_all_dom [in for_all_dom]
WProperties_fun.filter_dom [in filter_dom]
WProperties_fun.diff [in diff]
WProperties_fun.exists_range [in exists_range]
WProperties_fun.Partition [in Partition]
WProperties_fun.restrict [in restrict]
WProperties_fun.uncurry [in uncurry]
WProperties_fun.for_all [in for_all]
WProperties_fun.partition_dom [in partition_dom]
WProperties_fun.partition_range [in partition_range]
WProperties_fun.for_all_range [in for_all_range]
WRawSets.Empty [in Empty]
WRawSets.eq [in eq]
WRawSets.Equal [in Equal]
WRawSets.Exists [in Exists]
WRawSets.For_all [in For_all]
WRawSets.Subset [in Subset]
WRaw2SetsOn.add [in add]
WRaw2SetsOn.cardinal [in cardinal]
WRaw2SetsOn.choose [in choose]
WRaw2SetsOn.diff [in diff]
WRaw2SetsOn.elements [in elements]
WRaw2SetsOn.elt [in elt]
WRaw2SetsOn.empty [in empty]
WRaw2SetsOn.Empty [in Empty]
WRaw2SetsOn.eq [in eq]
WRaw2SetsOn.equal [in equal]
WRaw2SetsOn.Equal [in Equal]
WRaw2SetsOn.eq_dec [in eq_dec]
WRaw2SetsOn.Exists [in Exists]
WRaw2SetsOn.exists_ [in exists_]
WRaw2SetsOn.filter [in filter]
WRaw2SetsOn.fold [in fold]
WRaw2SetsOn.For_all [in For_all]
WRaw2SetsOn.for_all [in for_all]
WRaw2SetsOn.In [in In]
WRaw2SetsOn.inter [in inter]
WRaw2SetsOn.is_empty [in is_empty]
WRaw2SetsOn.mem [in mem]
WRaw2SetsOn.partition [in partition]
WRaw2SetsOn.remove [in remove]
WRaw2SetsOn.singleton [in singleton]
WRaw2SetsOn.Subset [in Subset]
WRaw2SetsOn.subset [in subset]
WRaw2SetsOn.t [in t]
WRaw2SetsOn.union [in union]
WSetsOn.Empty [in Empty]
WSetsOn.eq [in eq]
WSetsOn.Equal [in Equal]
WSetsOn.Exists [in Exists]
WSetsOn.For_all [in For_all]
WSetsOn.Subset [in Subset]
WSfun.elt [in elt]
WSfun.Empty [in Empty]
WSfun.Empty [in Empty]
WSfun.eq [in eq]
WSfun.Equal [in Equal]
WSfun.Equal [in Equal]
WSfun.Equiv [in Equiv]
WSfun.Equivb [in Equivb]
WSfun.eq_key_elt [in eq_key_elt]
WSfun.eq_key [in eq_key]
WSfun.Exists [in Exists]
WSfun.For_all [in For_all]
WSfun.In [in In]
WSfun.key [in key]
WSfun.Subset [in Subset]
WS_to_Finite_set.mkEns [in mkEns]
WS_to_Finite_set.mkEns [in mkEns]
ww_add [in ww_add]
ww_add_c [in ww_add_c]
ww_mod_gt_aux [in ww_mod_gt_aux]
ww_mul_c [in ww_mul_c]
ww_gcd_gt [in ww_gcd_gt]
ww_div_gt_aux [in ww_div_gt_aux]
ww_zdigits [in ww_zdigits]
ww_square_c [in ww_square_c]
ww_head0 [in ww_head0]
ww_sub_c [in ww_sub_c]
ww_div21 [in ww_div21]
ww_to_Z [in ww_to_Z]
ww_opp [in ww_opp]
ww_add_carry [in ww_add_carry]
ww_mod_gt [in ww_mod_gt]
ww_sub_carry_c [in ww_sub_carry_c]
ww_tail0 [in ww_tail0]
ww_sqrt [in ww_sqrt]
ww_div [in ww_div]
ww_gcd_gt_aux [in ww_gcd_gt_aux]
ww_add_mul_div [in ww_add_mul_div]
ww_mod [in ww_mod]
ww_digits [in ww_digits]
ww_karatsuba_c [in ww_karatsuba_c]
ww_pos_mod [in ww_pos_mod]
ww_div_gt [in ww_div_gt]
ww_0W [in ww_0W]
ww_gcd_gt_body [in ww_gcd_gt_body]
ww_opp_carry [in ww_opp_carry]
ww_W0 [in ww_W0]
ww_succ [in ww_succ]
ww_Bm1 [in ww_Bm1]
ww_pred_c [in ww_pred_c]
ww_opp_c [in ww_opp_c]
ww_add_c_cont [in ww_add_c_cont]
ww_head1 [in ww_head1]
ww_pred [in ww_pred]
ww_add_carry_c [in ww_add_carry_c]
ww_is_zero [in ww_is_zero]
ww_is_even [in ww_is_even]
ww_gcd [in ww_gcd]
ww_compare [in ww_compare]
ww_1 [in ww_1]
ww_WW [in ww_WW]
ww_sub_carry [in ww_sub_carry]
ww_mul [in ww_mul]
ww_sub [in ww_sub]
ww_succ_c [in ww_succ_c]
ww_sqrt2 [in ww_sqrt2]
w_2 [in w_2]
w_div32 [in w_div32]
w_mul_add [in w_mul_add]