Commit 2024-09-13 04:26 8ce56442

View on Github →

chore: deprecate plain Commutative, Associative (#16749) …in favour of Std.Commutative and Std.Associative. Also reorder Init.Logic so that non-deprecated code is at the top, and remove redundant [symm] attributes.

Estimated changes

modified theorem List.foldl1_eq_foldr1
modified theorem List.foldl_eq_foldr
modified theorem max_associative
modified theorem max_commutative
modified theorem max_left_commutative
modified theorem min_associative
modified theorem min_commutative
modified theorem min_left_commutative