max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fold Nat literals at reduce

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-18 17:10:01 -07:00
parent 1514e39006
commit a486503c62
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Meta/Reduce.lean
View file

@ -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)