diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean
index a6105dadc5..fb0aa38940 100644
--- a/src/Lean/Compiler/LCNF/ToMono.lean
+++ b/src/Lean/Compiler/LCNF/ToMono.lean
@@ -92,6 +92,8 @@ partial def LetValue.toMono (e : LetValue) (resultFVar : FVarId) : ToMonoM LetVa
       return args[1]!.toLetValue
     else if declName == ``Quot.mk || declName == ``Quot.lcInv then
       return args[2]!.toLetValue
+    else if declName == ``Nat.zero then
+      return .lit (.nat 0)
     else if declName == ``Nat.succ then
       -- This should have been handled in Code.toMono.
       unreachable!
diff --git a/tests/lean/doubleReset.lean.expected.out b/tests/lean/doubleReset.lean.expected.out
index f341b2caa4..42eefeb59c 100644
--- a/tests/lean/doubleReset.lean.expected.out
+++ b/tests/lean/doubleReset.lean.expected.out
@@ -15,7 +15,7 @@
             let x_8 : obj := proj[0] x_7;
             let x_9 : obj := proj[1] x_7;
             let x_18 : obj := reset[2] x_7;
-            let x_10 : obj := ctor_0[Nat.zero];
+            let x_10 : obj := 0;
             let x_11 : obj := Array.uset ◾ x_4 x_3 x_10 ◾;
             let x_12 : obj := reuse x_18 in ctor_0[Prod.mk] x_8 x_9;
             let x_13 : obj := reuse x_19 in ctor_0[Prod.mk] x_12 x_1;