[ new ] Add test for deriving spec list generators

UARTman · UARTman · commit ef9ac44b4a0f · 2026-01-18T16:42:31.000+03:00
diff --git a/tests/derivation/core/spec 001/DerivedGen.idr b/tests/derivation/core/spec 001/DerivedGen.idr
@@ -0,0 +1,20 @@
+module DerivedGen
+
+import RunDerivedGen
+
+%default total
+
+%language ElabReflection
+
+data X = MkX (List Nat)
+
+%hint
+XShow : Show X
+XShow = %runElab derive
+
+export
+checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty Nat) => Gen MaybeEmpty X
+checkedGen = deriveGen
+
+main : IO ()
+main = runGs [ G $ \fl => checkedGen fl @{smallNats} ]
diff --git a/tests/derivation/core/spec 001/RunDerivedGen.idr b/tests/derivation/core/spec 001/RunDerivedGen.idr
@@ -0,0 +1 @@
+../_common/RunDerivedGen.idr
diff --git a/tests/derivation/core/spec 001/derive.ipkg b/tests/derivation/core/spec 001/derive.ipkg
@@ -0,0 +1 @@
+../_common/derive.ipkg
diff --git a/tests/derivation/core/spec 001/expected b/tests/derivation/core/spec 001/expected
diff --git a/tests/derivation/core/spec 001/run b/tests/derivation/core/spec 001/run
@@ -0,0 +1 @@
+../_common/run
