aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ML4PG/libs/ssreflect/advance/bigop_names
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/ML4PG/libs/ssreflect/advance/bigop_names')
-rw-r--r--contrib/ML4PG/libs/ssreflect/advance/bigop_names157
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