- Sep 20, 2024
-
-
François Clément authored
-
- Sep 19, 2024
-
-
François Clément authored
antisym_compl <-> asym_compl, monomial_order -> monomial_order_incr, monomial_order_equiv_sto -> monomial_order_incr_equiv_sto, monomial_order_conv -> monomial_order_incr_conv, graded_monomial_order -> graded_monomial_order_incr. Modify trans_compl. Remove meaningless monomial_order_br_monoid_compat_min. Add transitive_incomparability, strict_weak_order, trans_inc_equiv, strict_weak_order_equiv_{spo,no_asym,no_irrefl}, conv_fix_equiv, compl_conv_eq, trans_inc_conv, trans_inc_compl, monomial_order, monomial_order_equiv_sto, monomial_order_conv, graded_monomial_order.
-
- Sep 18, 2024
-
-
François Clément authored
{,total}preorder_conv_equiv, {,strict_}{partial,total}_order_conv_equiv, {refl,irrefl,sym}_compl. WIP: {antisym,asym,trans,conn,str_conn}_compl.
-
François Clément authored
Modify monomial_order, monomial_order_equiv_sto, monomial_order_conv, {symlex,revlex}_monomial_order, Add bin_rel_monoid_compat_{min,max}, monomial_order_decr, monomial_order_decr_equiv_sto, monomial_order_br_monoid_compat_min, bin_rel_monoid_compat_{min,max}_conv, monomial_order_decr_conv, {lex,colex,symlex,revlex}_br_monoid_compat_{min,max}, graded_br_monoid_compat_{min,max}, graded_monomial_order_decr.
-
- Sep 17, 2024
-
-
François Clément authored
Add modus_ponens_and3. Monoid_compl: Add graded_{irrefl,trans,conn}, graded_{strict_partial_order,strict_total_order}, graded_{br_plus_compat_{l,r},zero_is_{min,max}}, graded_{br_monoid_compat_{l,r},monomial_order}. WIP: graded_zero_is_bound is False! TODO: properties of ordered monoids.
-
François Clément authored
{lex,colex,symlex,revlex}_zero_is_{min,max,bound}, {lex,colex,symlex,revlex}_br_monoid_compat_{l,r}, {lex,colex,symlex,revlex}_monomial_order. Add defs graded, gr{lex,colex,symlex,revlex}. Add graded_l. Signed-off-by:
François Clément <francois.clement@inria.fr>
-
François Clément authored
Add {lex,colex,symlex,revlex}_{nil,S}, {lex,colex,symlex,revlex}_{irrefl,trans,conn}, {lex,colex,symlex,revlex}_{strict_partial_order,strict_total_order}.
-
François Clément authored
Rename modus_ponens2 -> modus_ponens_and. Add modus_ponens_or. Monoid_compl: Add defs connected_alt{,_contra}, plus_is_reg_{l,r}, zero_is_{max,bound}. Modif defs bin_rel_monoid_compat_{l,r}, monomial_order. Rename monomial_order_plus_compat_{l,r} -> monomial_order_br_plus_compat_{l,r}. Rm useless monomial_order_zero_is_min. Add conn_equiv_contra, plus_is_reg_equiv, bin_rel_plus_compat_reg_{l,r}, bin_rel_plus_compat_is_reg_{l,r}, monomial_order_conn_alt{,_contra}, monomial_order_zero_is_bound, monomial_order_br_plus_reg_{l,r}, monomial_order_plus_is_reg_{l,r}, bin_rel_plus_{compat,reg}_{l,r}_conv, zero_is_{min,max,bound}_conv, bin_rel_monoid_compat_{l,r}_conv, monomial_order_conv.
-
Sylvie Boldo authored
-
François Clément authored
Add modus_ponens2, eq_sym_equiv. Monoid_compl: Rm useless strict_preorder (= strict_partial_order), monomial_order (for large ineq). Rename irrefl_asym -> irrefl_asym_w_trans, strict_monomial_order* -> monomial_order*. Add asym_antisym, irrefl_asym_w_antisym, asym_equiv, conn_equiv, str_conn_conn, {refl,irrefl,sym,antisym,asym,trans,conn,str_conn}_conv, {partial_equivalence_relation,equivalence_relation}_conv, {preorder,total_preorder,partial_order,total_order}_conv, {strict_partial_order,strict_total_order}_conv, bin_rel_monoid_compat_equiv, monomial_order_br_monoid_compat_{r,l}, monomial_order_zero_is_min. multi_index: Maj suggestions.
-
- Sep 16, 2024
-
-
François Clément authored
-
François Clément authored
-
François Clément authored
This should be in a separate file?
-
Sylvie Boldo authored
-
François Clément authored
-
- Sep 15, 2024
-
-
François Clément authored
-
- Sep 13, 2024
-
-
Sylvie Boldo authored
-
- Sep 12, 2024
-
-
Sylvie Boldo authored
-
- Sep 11, 2024
-
-
Sylvie Boldo authored
bof...
-
- Sep 10, 2024
-
-
François Clément authored
-
Sylvie Boldo authored
-
- Sep 07, 2024
-
-
Houda Mouhcine authored
-
- Sep 06, 2024
-
-
Houda Mouhcine authored
Signed-off-by:
Houda Mouhcine <houda.mouhcine@inria.fr>
-
- Sep 05, 2024
-
-
Sylvie Boldo authored
-
Sylvie Boldo authored
-
- Sep 04, 2024
-
-
Sylvie Boldo authored
-
- Aug 29, 2024
-
-
Sylvie Boldo authored
-
- Aug 27, 2024
-
-
Sylvie Boldo authored
-
- Aug 26, 2024
-
-
Sylvie Boldo authored
-
- Jul 30, 2024
-
-
François Clément authored
-
François Clément authored
-
- Jul 29, 2024
-
-
Houda Mouhcine authored
-
https://www-lipn.univ-paris13.fr/coq-num-analysisHouda Mouhcine authored
# Conflicts: # FEM/FE_LagP.v
-
Houda Mouhcine authored
-
François Clément authored
Rename gmS_{injS,bijS}_sub_equiv_alt -> gmS_{injS,bijS}_val_equiv, lmS_{injS,bijS}_sub_equiv_alt -> lmS_{injS,bijS}_val_equiv, lmS_{injS,bijS}_sub_equiv -> lmS_{injS,bijS}_val_equiv_alt, lmS_bijS_sub_full_equiv -> lmS_bijS_val_full_equiv, lmS_bijS_sub_gather_equiv -> lmS_bijS_val_gather_equiv.
-
François Clément authored
-
François Clément authored
-
François Clément authored
-
François Clément authored
-
François Clément authored
-