From 4fd2e71bc9aa0887d31611a6bee79ee4ade71282 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Sep 2018 14:56:31 -0700 Subject: [PATCH] chore(library/init/data/ordering/basic): mark `cmp_using` as `[inline]` --- library/init/data/ordering/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/data/ordering/basic.lean b/library/init/data/ordering/basic.lean index 9f8e7b80e0..79f839d7fa 100644 --- a/library/init/data/ordering/basic.lean +++ b/library/init/data/ordering/basic.lean @@ -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