From a486503c624cbb71cbea0954c8f0deedc0c0613d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 18 Mar 2022 17:10:01 -0700 Subject: [PATCH] chore: fold `Nat` literals at reduce --- src/Lean/Meta/Reduce.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean index 4589d494dc..066659cc08 100644 --- a/src/Lean/Meta/Reduce.lean +++ b/src/Lean/Meta/Reduce.lean @@ -31,7 +31,10 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta args ← args.modifyM i visit else args ← args.modifyM i visit - pure (mkAppN f args) + if f.isConstOf ``Nat.succ && args.size == 1 && args[0].isNatLit then + return mkRawNatLit (args[0].natLit?.get! + 1) + else + return mkAppN f args | Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b) | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b) | Expr.proj n i s .. => return mkProj n i (← visit s)