guard_msgs in test

src/Init/Data/Ord.lean

@@ -38,9 +38,10 @@ the same name by age (in descending order). (If all fields are sorted ascending
 order as they are listed in the structure, you can also use `deriving Ord` on the structure
 definition for the same effect.)
 -/
-@[macro_inline] def «then» : Ordering → Ordering → Ordering
-  | .eq, f => f
-  | o, _ => o
+@[macro_inline] def «then» (a b : Ordering) : Ordering :=
+  match a with
+  | .eq => b
+  | a => a
 
 /--
 Check whether the ordering is 'equal'.

tests/lean/run/Ord.lean

@@ -4,7 +4,7 @@ inductive SimpleInd
   | B
 deriving Ord
 
-mutual 
+mutual
 inductive Foo
   | A : Int → (3 = 3) → String → Foo
   | B : Bar → Foo
@@ -15,7 +15,7 @@ inductive Bar
 deriving Ord
 end
 
-inductive ManyConstructors | A | B | C | D | E | F | G | H | I | J | K | L 
+inductive ManyConstructors | A | B | C | D | E | F | G | H | I | J | K | L
   | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
 deriving Ord
 
@@ -40,3 +40,10 @@ deriving Ord
 inductive Fixed' : Type → Type 1 where
   | mk : Int → Fixed' α
 deriving Ord
+
+-- Before fixing the definition of `Ordering.then`, this would panic,
+-- because short-circuiting was not working.
+def foo (a : List Nat) := Ordering.then (compare a.length 1) (compare a[0]! 1)
+/-- info: Ordering.lt -/
+#guard_msgs in
+#eval foo []