From fbac0d2ddb9e6883a41a97bf44f20f753f6b24ce Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Sun, 18 May 2025 18:33:47 -0700 Subject: [PATCH] chore: use LitValue.toExpr instead of duplicating its definition (#8398) --- src/Lean/Compiler/LCNF/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean index 917ce9a6a8..d1eb4359f5 100644 --- a/src/Lean/Compiler/LCNF/Basic.lean +++ b/src/Lean/Compiler/LCNF/Basic.lean @@ -117,8 +117,7 @@ private unsafe def LetValue.updateArgsImp (e : LetValue) (args' : Array Arg) : L def LetValue.toExpr (e : LetValue) : Expr := match e with - | .lit (.nat val) => .lit (.natVal val) - | .lit (.str val) => .lit (.strVal val) + | .lit v => v.toExpr | .erased => erasedExpr | .proj n i s => .proj n i (.fvar s) | .const n us as => mkAppN (.const n us) (as.map Arg.toExpr)