Commit 2023-12-26 22:33 9757df4e

View on Github →

chore: remove workarounds for lean4#1891 (#9290) We no longer need to explicitly specify the Monotone and StrictMono arguments, after https://github.com/leanprover/lean4/commit/069873d8e5e0e7bed18f71edb63d18da50748ec9 fixed https://github.com/leanprover/lean4/issues/1891. Compare to the mathlib3 declarations: https://github.com/leanprover-community/mathlib/blob/65a1391a0106c9204fe45bc73a039f056558cb83/src/data/prod/lex.lean#L93-L107

Estimated changes