From 2734facb89861d606c4b60861638e519dc8491e2 Mon Sep 17 00:00:00 2001
From: Jesper Cockx <jesper@sikanda.be>
Date: Wed, 26 Aug 2026 16:07:55 +0200
Subject: [PATCH] Add special rules for Nat zero and suc constructors

---
 src/Agda2Hs/Compile/Name.hs |  2 ++
 test/Succeed/ZeroSuc.agda   | 26 ++++++++++++++++++++++++++
 test/Succeed/ZeroSuc.hs     | 17 +++++++++++++++++
 3 files changed, 45 insertions(+)
 create mode 100644 test/Succeed/ZeroSuc.agda
 create mode 100644 test/Succeed/ZeroSuc.hs

diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs
index ae24fa54..8998188c 100644
--- a/src/Agda2Hs/Compile/Name.hs
+++ b/src/Agda2Hs/Compile/Name.hs
@@ -65,6 +65,8 @@ toNameImport x (Just mod) =
 defaultSpecialRules :: SpecialRules
 defaultSpecialRules = Map.fromList
   [ "Agda.Builtin.Nat.Nat"          `to` "Natural"      `importing` Just "Numeric.Natural"
+  , "Agda.Builtin.Nat.Nat.zero"     `to` "0"            `importing` Nothing
+  , "Agda.Builtin.Nat.Nat.suc"      `to` "succ"         `importing` Nothing
   , "Haskell.Prelude.coerce"        `to` "unsafeCoerce" `importing` Just "Unsafe.Coerce"
   , "Agda.Builtin.Int.Int"          `to` "Integer"      `importing` Nothing
   , "Agda.Builtin.Word.Word64"      `to` "Word"         `importing` Nothing
diff --git a/test/Succeed/ZeroSuc.agda b/test/Succeed/ZeroSuc.agda
new file mode 100644
index 00000000..0deae2f0
--- /dev/null
+++ b/test/Succeed/ZeroSuc.agda
@@ -0,0 +1,26 @@
+module ZeroSuc where
+
+open import Haskell.Prelude
+
+test1 : Nat
+test1 = zero
+
+{-# COMPILE AGDA2HS test1 #-}
+
+test2 : Nat → Nat
+test2 = suc
+
+{-# COMPILE AGDA2HS test2 #-}
+
+data MyNat : Set where
+  MyZero : MyNat
+  MySuc : MyNat → MyNat
+
+{-# COMPILE AGDA2HS MyNat #-}
+
+opaque
+  test3 : MyNat → Nat
+  test3 MyZero = zero
+  test3 (MySuc n) = suc (test3 n)
+
+{-# COMPILE AGDA2HS test3 #-}
diff --git a/test/Succeed/ZeroSuc.hs b/test/Succeed/ZeroSuc.hs
new file mode 100644
index 00000000..976da3d1
--- /dev/null
+++ b/test/Succeed/ZeroSuc.hs
@@ -0,0 +1,17 @@
+module ZeroSuc where
+
+import Numeric.Natural (Natural)
+
+test1 :: Natural
+test1 = 0
+
+test2 :: Natural -> Natural
+test2 = succ
+
+data MyNat = MyZero
+           | MySuc MyNat
+
+test3 :: MyNat -> Natural
+test3 MyZero = 0
+test3 (MySuc n) = succ (test3 n)
+