From 3ead33bd13a4497bc0bdf76f2248088c65f6f3cb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Feb 2024 15:18:30 -0800 Subject: [PATCH] chore: `isNatLit` => `isRawNatLit` --- src/Lean/Meta/LazyDiscrTree.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean index 43c6b20c677e..7f58f8767fa1 100644 --- a/src/Lean/Meta/LazyDiscrTree.lean +++ b/src/Lean/Meta/LazyDiscrTree.lean @@ -98,7 +98,7 @@ private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Arr - `Nat.succ x` where `isNumeral x` - `OfNat.ofNat _ x _` where `isNumeral x` -/ private partial def isNumeral (e : Expr) : Bool := - if e.isNatLit then true + if e.isRawNatLit then true else let f := e.getAppFn if !f.isConst then false