From 6220dc39248d385b94a154d8185d594e85687808 Mon Sep 17 00:00:00 2001
From: arthur-adjedj <arthur.adjedj@gmail.com>
Date: Thu, 21 Mar 2024 08:39:07 +0100
Subject: [PATCH] fix: ignore unused alternatives in `Ord` derive handler

Closes #3706
This derive handler's implementation is very similar to `BEq`'s, which already ignores unused alternative so as to work correctly on indexed inductive types. This PR simply implements the same solution as the one present in `BEq.lean`.
---
 src/Lean/Elab/Deriving/Ord.lean |  1 +
 tests/lean/run/3706.lean        | 13 +++++++++++++
 2 files changed, 14 insertions(+)
 create mode 100644 tests/lean/run/3706.lean

diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean
index 47a4bcfc1ebf..1b67f532adf8 100644
--- a/src/Lean/Elab/Deriving/Ord.lean
+++ b/src/Lean/Elab/Deriving/Ord.lean
@@ -84,6 +84,7 @@ def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   for i in [:ctx.typeInfos.size] do
     auxDefs := auxDefs.push (← mkAuxFunction ctx i)
   `(mutual
+     set_option match.ignoreUnusedAlts true
      $auxDefs:command*
     end)
 
diff --git a/tests/lean/run/3706.lean b/tests/lean/run/3706.lean
new file mode 100644
index 000000000000..da8acce2a5c2
--- /dev/null
+++ b/tests/lean/run/3706.lean
@@ -0,0 +1,13 @@
+/--Ensure that `deriving Ord` works on indexed inductive types.-/
+inductive Ty where
+  | int
+  | bool
+inductive Expr : Ty → Type where
+  | a : Expr .int
+  | b : Expr .bool
+deriving Ord
+
+inductive Vec (α : Type u) : Nat → Type u
+  | nil  : Vec α 0
+  | cons : α → {n : Nat} → Vec α n → Vec α (n+1)
+deriving Ord