diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean index 43c6b20c67..7f58f8767f 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