*): use `[nonempty _]` instead of `(_ : nonempty _)` (#3526)

Commit

5 years ago

chore(order/filter/*): use `[nonempty _]` instead of `(_ : nonempty _)` (#3526) In most cases Lean can find an instance automatically.

Author

urkud

Parents