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