chore(library/init/data/ordering/basic): mark cmp_using as [inline]

This commit is contained in:
Leonardo de Moura 2018-09-17 14:56:31 -07:00
parent 5d455bf10a
commit 4fd2e71bc9

View file

@ -31,7 +31,7 @@ theorem swap_swap : ∀ (o : ordering), o.swap.swap = o
| gt := rfl
end ordering
def cmp_using {α : Type u} (lt : αα → Prop) [decidable_rel lt] (a b : α) : ordering :=
@[inline] def cmp_using {α : Type u} (lt : αα → Prop) [decidable_rel lt] (a b : α) : ordering :=
if lt a b then ordering.lt
else if lt b a then ordering.gt
else ordering.eq