From 765f98770bb2d9b20982c77ffa669e903420587a Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 7 Jul 2025 20:36:34 -0700
Subject: [PATCH] chore: improve pattern matching (#9242)

---
 src/Lean/Compiler/IR/ToIR.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index 7c1a741dfa..ac2cb719f1 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -137,10 +137,8 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
   | .proj typeName i fvarId =>
     match (← get).fvars[fvarId]? with
     | some (.var varId) =>
-      -- TODO: have better pattern matching here
-      let some (.inductInfo { ctors, .. }) := (← Lean.getEnv).find? typeName
-        | panic! "projection of non-inductive type"
-      let ctorName := ctors[0]!
+      let some (.inductInfo { ctors := [ctorName], .. }) := (← Lean.getEnv).find? typeName
+        | panic! "projection of non-structure type"
       let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
       let ⟨result, type⟩ := lowerProj varId ctorInfo fields[i]!
       match result with