From 8e5a3e416bdc9b6e4a0cb6634ed92cf479494d4f Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Tue, 14 Jan 2025 15:32:54 -0800 Subject: [PATCH] chore: remove duplicate branch in LCNF.toMonoType (#6644) --- src/Lean/Compiler/LCNF/MonoTypes.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Lean/Compiler/LCNF/MonoTypes.lean b/src/Lean/Compiler/LCNF/MonoTypes.lean index 924ab80cccb7..ce366b187d23 100644 --- a/src/Lean/Compiler/LCNF/MonoTypes.lean +++ b/src/Lean/Compiler/LCNF/MonoTypes.lean @@ -74,8 +74,6 @@ partial def toMonoType (type : Expr) : CoreM Expr := do let type := type.headBeta if type.isErased then return erasedExpr - else if type.isErased then - return erasedExpr else if isTypeFormerType type then return erasedExpr else match type with