Derive is_antisymm

Stream: Is there code for X?

[Marcus Rossel]

Is there an easy way to get is_antisymm for tag's ≤ here?

@[derive has_le, derive has_lt]
def tag := lex ℕ ℕ

[Gabriel Ebner]

I would just derive linear_order directly and avoid the is_antisymm type class:

import order.lexicographic
import order.rel_classes

@[derive linear_order]
def tag := lex ℕ ℕ

example : is_antisymm tag (≤) := by apply_instance