diff options
Diffstat (limited to 'contrib/ML4PG/libs/ssreflect/advance/bigop_names')
-rw-r--r-- | contrib/ML4PG/libs/ssreflect/advance/bigop_names | 157 |
1 files changed, 0 insertions, 157 deletions
diff --git a/contrib/ML4PG/libs/ssreflect/advance/bigop_names b/contrib/ML4PG/libs/ssreflect/advance/bigop_names deleted file mode 100644 index d228e3ab..00000000 --- a/contrib/ML4PG/libs/ssreflect/advance/bigop_names +++ /dev/null @@ -1,157 +0,0 @@ -1 mulC_id -2 mulC_zero -3 mulC_dist -4 mul1m -5 mulm1 -6 mulmA -7 iteropE -8 mulmC -9 mulmCA -10 mulmAC -11 mulmACA -12 mul0m -13 mulm0 -14 addmA -15 addmC -16 addmCA -17 addmAC -18 add0m -19 addm0 -20 mulm_addl -21 mulm_addr -22 bigopE -23 mem_index_iota -24 mem_index_enum -25 filter_index_enum -26 big_load -27 big_rec3 -28 big_ind3 -29 big_rec2 -30 big_ind2 -31 big_morph -32 big_rec -33 big_ind -34 eq_big_op -35 big_endo -36 big_filter -37 big_filter_cond -38 eq_bigl -39 big_andbC -40 eq_bigr -41 eq_big -42 congr_big -43 big_nil -44 big_cons -45 big_map -46 big_nth -47 big_hasC -48 big_pred0_eq -49 big_pred0 -50 big_cat_nested -51 big_catl -52 big_catr -53 big_const_seq -54 big_seq_cond -55 big_seq -56 eq_big_seq -57 big_nat_cond -58 big_nat -59 congr_big_nat -60 eq_big_nat -61 big_geq -62 big_ltn_cond -63 big_ltn -64 big_addn -65 big_add1 -66 big_nat_recl -67 big_mkord -68 big_nat_widen -69 big_ord_widen_cond -70 big_ord_widen -71 big_ord_widen_leq -72 big_ord0 -73 big_tnth -74 big_ord_narrow_cond -75 big_ord_narrow_cond_leq -76 big_ord_narrow -77 big_ord_narrow_leq -78 big_ord_recl -79 big_const -80 big_const_nat -81 big_const_ord -82 eq_big_idx_seq -83 eq_big_idx -84 big1_eq -85 big1 -86 big1_seq -87 big_seq1 -88 big_mkcond -89 big_cat -90 big_pred1_eq -91 big_pred1 -92 big_cat_nat -93 big_nat1 -94 big_nat_recr -95 big_ord_recr -96 big_sumType -97 big_split_ord -98 eq_big_perm -99 big_uniq -100 big_index_uniq -101 big_rem -102 big_undup -103 eq_big_idem -104 big_split -105 bigID -106 bigU -107 bigD1 -108 bigD1_seq -109 cardD1x -110 partition_big -111 reindex_onto -112 reindex -113 reindex_inj -114 big_nat_rev -115 pair_big_dep -116 pair_big -117 pair_bigA -118 exchange_big_dep -119 exchange_big -120 exchange_big_dep_nat -121 exchange_big_nat -122 big_distrl -123 big_distrr -124 big_distrlr -125 big_distr_big_dep -126 big_distr_big -127 bigA_distr_big_dep -128 bigA_distr_big -129 bigA_distr_bigA -130 big_has -131 big_all -132 big_has_cond -133 big_all_cond -134 big_orE -135 big_andE -136 sum_nat_const -137 sum1_card -138 prod_nat_const -139 sum_nat_const_nat -140 prod_nat_const_nat -141 leqif_sum -142 leq_sum -143 sum_nat_eq0 -144 prodn_cond_gt0 -145 prodn_gt0 -146 leq_bigmax_cond -147 leq_bigmax -148 bigmax_leqP -149 bigmax_sup -150 bigmax_eq_arg -151 eq_bigmax_cond -152 eq_bigmax -153 expn_sum -154 dvdn_biglcmP -155 biglcmn_sup -156 dvdn_biggcdP -157 biggcdn_inf |