From d6675225243ba5205bcd46eced5926b027a39869 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Wed, 16 Jul 2025 16:41:41 -0700 Subject: [PATCH] refactor: remove special cases for subsingleton casesOn (#9412) --- src/Lean/Compiler/LCNF/ToLCNF.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 6fa84aeb14..4d1b114a46 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -685,15 +685,13 @@ where visitQuotLift e else if declName == ``Quot.mk then visitCtor 3 e - else if declName == ``Eq.casesOn || declName == ``Eq.rec || declName == ``Eq.recOn || declName == ``Eq.ndrec then + else if declName == ``Eq.rec || declName == ``Eq.recOn || declName == ``Eq.ndrec then visitEqRec e - else if declName == ``HEq.casesOn || declName == ``HEq.rec || declName == ``HEq.ndrec then + else if declName == ``HEq.rec || declName == ``HEq.ndrec then visitHEqRec e else if declName == ``And.rec || declName == ``Iff.rec then visitAndIffRecCore e (minorPos := 3) - else if declName == ``And.casesOn || declName == ``Iff.casesOn then - visitAndIffRecCore e (minorPos := 4) - else if declName == ``False.rec || declName == ``Empty.rec || declName == ``False.casesOn || declName == ``Empty.casesOn then + else if declName == ``False.rec || declName == ``Empty.rec then visitFalseRec e else if declName == ``lcUnreachable then visitLcUnreachable e