diff --git a/.editorconfig b/.editorconfig
index 569258485..0f2df35fc 100644
--- a/.editorconfig
+++ b/.editorconfig
@@ -48,3 +48,18 @@ max_line_length = off
[*.py]
indent_size = 4
+
+# See: https://stackoverflow.com/a/40348831/2572373
+[**{.build,docs/build,linters/build}**]
+charset = unset
+end_of_line = unset
+insert_final_newline = unset
+trim_trailing_whitespace = unset
+indent_style = unset
+indent_size = unset
+max_line_length = unset
+
+# Auto-generated file
+[.idrisCommit]
+insert_final_newline = unset
+
diff --git a/.github/workflows/ci-super-linter.yml b/.github/workflows/ci-super-linter.yml
index 988b6d15e..070d6f9b5 100644
--- a/.github/workflows/ci-super-linter.yml
+++ b/.github/workflows/ci-super-linter.yml
@@ -42,20 +42,13 @@ jobs:
fetch-depth: 0
persist-credentials: false # https://docs.zizmor.sh/audits/#artipacked
+ - name: Load super-linter configuration
+ # Use grep inverse matching to exclude eventual comments in the .env file
+ # because the GitHub Actions command to set environment variables doesn't
+ # support comments.
+ run: grep -v '^#' .github/linters/super-linter.env >> "$GITHUB_ENV"
+
- name: Lint Code Base
uses: super-linter/super-linter/slim@v8
env:
- DEFAULT_BRANCH: master
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- IGNORE_GENERATED_FILES: true
- SAVE_SUPER_LINTER_SUMMARY: true # Required for generating linting reports in PR
-
- VALIDATE_PYTHON_BLACK: false # Avoid conflict: Ruff is preferred
- VALIDATE_GIT_COMMITLINT: false
-
- VALIDATE_MARKDOWN_PRETTIER: false # We use markdownlint
- VALIDATE_YAML_PRETTIER: false # We use yamllint
-
- # Disable Biome
- VALIDATE_BIOME_FORMAT: false
- VALIDATE_BIOME_LINT: false
diff --git a/.linters/super-linter-fix.ipkg b/.linters/super-linter-fix.ipkg
new file mode 100644
index 000000000..c60283e3f
--- /dev/null
+++ b/.linters/super-linter-fix.ipkg
@@ -0,0 +1,3 @@
+package super-linter-fix
+
+prebuild = "FIX_MARKDOWN=true FIX_NATURAL_LANGUAGE=true FIX_SPELL_CODESPELL=true ./super-linter.sh"
diff --git a/.linters/super-linter-local.env b/.linters/super-linter-local.env
new file mode 100644
index 000000000..b23a2a02a
--- /dev/null
+++ b/.linters/super-linter-local.env
@@ -0,0 +1,2 @@
+# Disable stuff which may not work for local run
+VALIDATE_CHECKOV=false
diff --git a/.linters/super-linter-run.ipkg b/.linters/super-linter-run.ipkg
new file mode 100644
index 000000000..10b181c4a
--- /dev/null
+++ b/.linters/super-linter-run.ipkg
@@ -0,0 +1,3 @@
+package super-linter-run
+
+prebuild = "./super-linter.sh"
diff --git a/.linters/super-linter.env b/.linters/super-linter.env
new file mode 100644
index 000000000..ba32c1a01
--- /dev/null
+++ b/.linters/super-linter.env
@@ -0,0 +1,17 @@
+DEFAULT_BRANCH=master
+IGNORE_GENERATED_FILES=true
+# Required for generating linting reports in PR
+SAVE_SUPER_LINTER_SUMMARY=true
+
+# Avoid conflict: Ruff is preferred
+VALIDATE_GIT_COMMITLINT=false
+VALIDATE_PYTHON_BLACK=false
+
+# We use markdownlint
+VALIDATE_MARKDOWN_PRETTIER=false
+# We use yamllint
+VALIDATE_YAML_PRETTIER=false
+
+# Disable Biome
+VALIDATE_BIOME_FORMAT=false
+VALIDATE_BIOME_LINT=false
diff --git a/.linters/super-linter.sh b/.linters/super-linter.sh
new file mode 100755
index 000000000..6601cdbdb
--- /dev/null
+++ b/.linters/super-linter.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+# See: https://github.com/super-linter/super-linter/blob/dd82ec5c927bff0fecc98865b0be8aa6ef849001/docs/run-linter-locally.md
+docker run --platform linux/amd64 \
+ --env-file "$(pwd)/../.github/linters/super-linter.env" \
+ --env-file "$(pwd)/../.github/linters/super-linter-local.env" \
+ -e LOG_LEVEL=NOTICE \
+ -e RUN_LOCAL=true \
+ -e FIX_MARKDOWN="${FIX_MARKDOWN:-false}" \
+ -e FIX_NATURAL_LANGUAGE="${FIX_NATURAL_LANGUAGE:-false}" \
+ -e FIX_SPELL_CODESPELL="${FIX_SPELL_CODESPELL:-false}" \
+ -v "$(pwd)/../":/tmp/lint \
+ ghcr.io/super-linter/super-linter:latest
diff --git a/docs/source/tutorials.rst b/docs/source/tutorials.rst
index fc8be5383..d4855c012 100644
--- a/docs/source/tutorials.rst
+++ b/docs/source/tutorials.rst
@@ -14,6 +14,14 @@ You can read more in the `original framework `_
:maxdepth: 1
:caption: Choose what to learn
- tutorials/test-function
- tutorials/generators
- tutorials/derivation
+ tutorials/t00-installation-and-setup
+ tutorials/t01-generator-monad
+ tutorials/t02-handling-emptiness
+ tutorials/t03-measuring-test-coverage
+ tutorials/t04-automatic-generator-derivation
+ tutorials/t05-derivegen-signatures
+ tutorials/t06-mixing-manual-and-automatic
+ tutorials/t07-beyond-fuel
+ tutorials/t08-generating-gadts-with-proofs
+ tutorials/t09-toy-example
+ tutorials/t10-derivation-tuning
diff --git a/docs/source/tutorials/derivation.md b/docs/source/tutorials/derivation.md
deleted file mode 100644
index 14eaabc00..000000000
--- a/docs/source/tutorials/derivation.md
+++ /dev/null
@@ -1 +0,0 @@
-# Automatic derivation of generators
diff --git a/docs/source/tutorials/generators.md b/docs/source/tutorials/generators.md
deleted file mode 100644
index eb61ce7b6..000000000
--- a/docs/source/tutorials/generators.md
+++ /dev/null
@@ -1 +0,0 @@
-# Hand-written generators
diff --git a/docs/source/tutorials/t00-installation-and-setup.md b/docs/source/tutorials/t00-installation-and-setup.md
new file mode 100644
index 000000000..e30181872
--- /dev/null
+++ b/docs/source/tutorials/t00-installation-and-setup.md
@@ -0,0 +1,186 @@
+# Installation and First Steps
+
+Welcome to DepTyCheck! This tutorial will guide you through installing Idris 2 and DepTyCheck, creating your first project, and running a simple
+generator.
+
+## Our Goal
+
+In this tutorial, you will:
+
+1. Install Idris 2 and the DepTyCheck library
+2. Create a project configured with DepTyCheck
+3. Write and run a generator that produces random `TrafficLight` values
+
+By the end, you will see output like:
+
+```text
+Red : TrafficLight
+```
+
+---
+
+## Step 1: Install Idris 2
+
+First, you need to install Idris 2. We recommend using [`pack`](https://github.com/stefan-hoeck/idris2-pack/), which manages both the compiler
+and library dependencies.
+
+Follow its [installation script](https://github.com/stefan-hoeck/idris2-pack/?tab=readme-ov-file#quick-installation).
+
+**Verify your installation:**
+
+```bash
+idris2 --version
+```
+
+Sample output:
+
+```text
+Idris 2, version 0.8.0-80fd5e4d7
+```
+
+```{note}
+You need Idris 2 version **0.8.0 or newer** for DepTyCheck to work.
+```
+
+---
+
+## Step 2: Create Your First Project
+
+### Create a project directory
+
+```bash
+mkdir deptycheck-tutorial
+cd deptycheck-tutorial
+```
+
+### Create a project file named `tutorial.ipkg`
+
+```text
+package tutorial
+
+version = 0.0.1
+langversion >= 0.8.0
+
+sourcedir = "."
+builddir = ".build"
+
+modules = Main
+main = Main
+executable = tutorial
+
+depends = deptycheck
+```
+
+```{note}
+The `depends = deptycheck` line tells Idris to use the DepTyCheck library.
+```
+
+---
+
+## Step 3: Write Your First Generator
+
+### Create a file `Main.idr` with the following code
+
+```idris
+import Deriving.DepTyCheck.Gen
+import System.Random.Pure.StdGen
+
+data TrafficLight = Red | Yellow | Green
+
+Show TrafficLight where
+ show Red = "Red"
+ show Yellow = "Yellow"
+ show Green = "Green"
+
+genTrafficLight : Fuel -> Gen MaybeEmpty TrafficLight
+genTrafficLight = deriveGen
+
+main : IO ()
+main = do
+ Just light <- pick (genTrafficLight (limit 0))
+ | Nothing => putStrLn "Generation failed"
+ printLn light
+```
+
+```{note}
+- `%language ElabReflection` enables the metaprogramming features needed for `deriveGen`
+- `deriveGen` automatically creates a generator for `TrafficLight`
+- `pick` runs the generator and extracts one value
+```
+
+---
+
+## Step 4: Build and Run
+
+### Build the project
+
+```bash
+pack build
+```
+
+`pack` will download and build all dependencies automatically along with source code of the module.
+
+### Run the executable
+
+```bash
+pack run tutorial.ipkg
+```
+
+Expected output (your result will vary):
+
+```text
+Yellow
+```
+
+```{note}
+Run the command multiple times to see different results (Yellow, Green, Red).
+```
+
+---
+
+## Step 4: Try It in the REPL (Optional)
+
+You can also test your generator interactively.
+
+### Start the REPL
+
+Pass the Main module name to preload it:
+
+```bash
+rlwrap pack repl ./Main.idr
+```
+
+```{note}
+- `%language ElabReflection` enables the metaprogramming features needed for `deriveGen`
+- `deriveGen` automatically creates a generator for `TrafficLight`
+- `pick` runs the generator and extracts one value
+```
+
+### Run the generator
+
+```text
+:exec printLn =<< pick (genTrafficLight (limit 0))
+```
+
+Expected output:
+
+```text
+Just Green
+```
+
+### Run it multiple times to see different colors
+
+### Exit the REPL
+
+```text
+:quit
+```
+
+---
+
+## Next Steps
+
+Now that you have a working setup, you are ready to learn the fundamentals of generator creation:
+
+- **Continue to Tutorial 1:** [The Generator Monad](t01-generator-monad.md) to learn how to create generators manually using `pure`, `elements`,
+ `choose`, and other combinators.
diff --git a/docs/source/tutorials/t01-generator-monad.md b/docs/source/tutorials/t01-generator-monad.md
new file mode 100644
index 000000000..4019aceb7
--- /dev/null
+++ b/docs/source/tutorials/t01-generator-monad.md
@@ -0,0 +1,308 @@
+# 1. The Generator Monad: Your First Generator
+
+Welcome to `DepTyCheck`! This tutorial is a hands-on guide that will help you learn the most important skill in property-based testing: generating
+random test data.
+
+We will keep things practical and focus on what you need to get started. You'll write code, run it, and see the results immediately.
+
+## Our Goal
+
+In this tutorial, we will guide you step by step to create a generator for the following `UserProfile` data type:
+
+```text
+data UserProfile = MkProfile String Nat
+```
+
+By the end, you will have a working program that produces random user profiles, like this:
+
+```text
+MkProfile "Alice" 37 : UserProfile
+```
+
+## Prerequisites
+
+This tutorial assumes you have completed [Installation and First Steps](t00-installation-and-setup.md) and have a working Idris 2 installation with
+DepTyCheck
+configured for your `tutorial.ipkg`.
+
+---
+
+## Step 1: Your First Generator
+
+Let's start by creating a generator that always produces the _same_ value. This will confirm our setup is working.
+
+### Create a new file named `Tutorial.idr`
+
+```idris
+import Test.DepTyCheck.Gen
+import Data.Vect
+
+%language ElabReflection
+```
+
+### Add the following code to it. We'll define our data type and import the necessary `DepTyCheck` modules
+
+```idris
+data UserProfile = MkProfile String Nat
+
+Show UserProfile where
+ show (MkProfile s y) = "MkProfile " ++ show s ++ " " ++ show y
+
+-- A generator that always produces the same, constant user profile
+genConstantUser : Gen1 UserProfile
+genConstantUser = pure (MkProfile "Alice" 30)
+```
+
+```{note}
+The `pure` function creates the simplest possible "recipe": one that always returns the exact value you give it. The type `Gen1` means this generator
+is guaranteed to produce a value.
+```
+
+### Run your generator
+
+To test your first generator lets do the following:
+
+```bash
+echo -e ':exec printLn =<< pick1 genConstantUser' |
+ rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr
+```
+
+Here we do:
+
+| | |
+| --- | ---------- |
+| `echo -e` and `\|` | We are going to run Idris2 in REPL mode, pass the input, wait for the output and close |
+| `:exec` | It is actually the Idris2 REPL command to run something in `IO` monad. For `:exec ?wat` the `?wat` is `IO _`. |
+| `printLn =<<` | Runs generator and prints output. `:exec` alone drops results; this shows them. |
+| `pick1 genConstantUser` | _We are very close, that's what is needed._ |
+| `rlwrap` | Not strictly needed for single runs, but reminds that Idris2 REPL lacks readline support |
+| `pack` | DepTyCheck depends on a set of libraries, so, `pack` launches `idris2` with the full set of required things |
+| `--extra-args="--no-banner"` | Reduces REPL output noise. Passes flag to hide Idris2 welcome banner |
+| `repl` | It actually instructs `pack` to run `idris2` in REPL mode |
+
+You will see an output, similar to the following:
+
+```text
+MkProfile "Alice" 30
+```
+
+You've just created and run your first generator! Now, let's make it more interesting by adding some randomness.
+
+---
+
+## Step 2: Adding Randomness
+
+Instead of a fixed age, let's generate a random one. We'll use the `choose` function for this.
+
+### Modify your file to create a new generator
+
+```idris
+-- A generator for a user with a random age between 18 and 99
+genRandomAgeUser : Gen1 UserProfile
+genRandomAgeUser = MkProfile "Alice" <$> choose (18, 99)
+```
+
+Here's what's new:
+
+- `choose (18, 99)` creates a recipe for picking a random number in that range.
+
+```{note}
+The `choose` function randomly picks between two generators with equal probability (50/50). This gives you a simple way to add variation to your
+generators.
+```
+
+- The `<$>` operator takes the result from the recipe on the right (our random number) and feeds it into the function on the left (`MkProfile "Alice"`).
+
+### Run it multiple times
+
+```bash
+echo -e ':exec printLn =<< pick1 genRandomAgeUser' |
+ rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr
+```
+
+```bash
+echo -e ':exec printLn =<< pick1 genRandomAgeUser' |
+ rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr
+```
+
+This time, you'll see a different result with each run:
+
+```text
+MkProfile "Alice" 22
+MkProfile "Alice" 35
+```
+
+Success! You've introduced randomness into your data.
+
+---
+
+## Step 3: Combining Two Random Generators
+
+Now, let's make the name random too. We need to combine two different random recipes.
+
+### Add a new generator that combines a random name and a random age
+
+```idris
+-- A generator for a user with a random name and a random age
+genUserProfile : Gen1 UserProfile
+genUserProfile = MkProfile <$> elements ["Alice", "Bob", "Charlie"] <*> choose (18, 99)
+```
+
+Here's the change:
+
+- `elements ["Alice", "Bob", "Charlie"]` creates a recipe for picking a random name from a list.
+- The `<*>` operator is the key: it lets us combine two recipes. It runs the name recipe and the age recipe, then feeds _both_ results into `MkProfile`.
+
+### Run your new generator a few times
+
+```bash
+echo -e ':exec printLn =<< pick1 genUserProfile' |
+ rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr
+```
+
+```bash
+echo -e ':exec printLn =<< pick1 genUserProfile' |
+ rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr
+```
+
+You'll now see completely random user profiles!
+
+```text
+MkProfile "Alice" 33
+MkProfile "Bob" 47
+```
+
+---
+
+## Step 4: Choosing Between Generators
+
+What if you want to generate more varied data? For example, maybe you want to generate a user who is either an "Admin" or a "Guest", with "Guest" being
+more common.
+
+`DepTyCheck` provides `oneOf` for equal choices and `frequency` for weighted choices.
+
+### Add these new generators to your file
+
+```idris
+-- A generator for a user role, with each role having an equal chance
+genRole : Gen1 String
+genRole = oneOf [pure "Admin", pure "User", pure "Guest"]
+
+-- A generator for a user type, where "Standard" is 4x more likely than "Premium"
+genUserType : Gen1 String
+genUserType = frequency [ (4, pure "Standard"), (1, pure "Premium") ]
+```
+
+- `oneOf` takes a list of generators and chooses one of them with equal probability.
+- `frequency` takes a list of `(weight, generator)` pairs. The weights determine the probability. Here, there are 5 total "parts" (4+1), so "Standard"
+has a 4/5 chance and "Premium" has a 1/5 chance.
+
+### Run them in the REPL
+
+```bash
+echo -e ':exec printLn =<< pick1 genRole' |
+ rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr
+```
+
+```bash
+echo -e ':exec printLn =<< pick1 genUserType' |
+ rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr
+```
+
+Sample output:
+
+```text
+"Guest"
+"Standard"
+```
+
+If you run `pick1 genUserType` many times, you will notice that `"Standard"` appears much more often than `"Premium"`.
+
+---
+
+## Step 5: Dependent Generation
+
+So far, the random values we've generated (name, age) have been independent of each other. But what if the **type** of one value needs to depend on the
+_value_ of another?
+
+This is the core challenge of generating dependent types. For example, let's generate a pair containing a random length `n` and a `Vect` that has
+exactly `n` elements. The type `Vect n Bool` depends directly on the value `n`.
+
+This is called **dependent generation**. We must first generate `n`, and _then_ use that value to create a generator for a vector of that specific type.
+We use `do` notation for this.
+
+### Add this generator to `Tutorial.idr`. It will create a dependent pair `(n ** Vect n Bool)`
+
+```idris
+-- A generator for a dependent pair: a random length `n` and a vector of that length
+genDependentVect : Gen1 (n ** Vect n Bool)
+genDependentVect = do
+ n <- choose (1, 5) -- Step 1: Generate a random length `n`
+ vec <- vectOf {n} (elements [True, False]) -- Step 2: Generate a vector of that exact length
+ pure (n ** vec) -- Step 3: Package them into a dependent pair with (**)
+```
+
+This `do` block is a sequence of dependent instructions:
+
+1. `n <- choose (1, 5)`: A random `Nat` is generated. Let's say the result is `3`.
+2. `vec <- vectOf {n} ...`: _Because_ `n` has the value `3`, this line creates and runs a generator for the type `Vect 3 Bool`. We have to pass it as a
+named argument because it is used at the type definition of `vectOf`.
+3. `pure (n ** vec)`: The value `3` and the generated vector (e.g., `[True, False, True]`) are bundled into a dependent pair using the `**` constructor.
+
+Run it in the REPL:
+
+```bash
+echo -e ':exec printLn =<< pick1 genDependentVect' |
+ rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr
+```
+
+For multiple times the output might be:
+
+```text
+(3 ** [False, False, False])
+(5 ** [True, True, True, True, True])
+(2 ** [True, False])
+```
+
+Notice that the length of the vector in the output always matches the number next to it. This powerful technique is what allows `DepTyCheck` to generate
+valid data for complex, dependent types.
+
+---
+
+## Step 6: Generating a Collection
+
+Finally, let's generate a list of test users. You can use the `listOf` combinator to run your generator multiple times and collect the results.
+
+### Add one last generator to your `Tutorial.idr` file
+
+```idris
+-- A generator that produces a list of 5 random user profiles
+genFiveUsers : Gen1 (List UserProfile)
+genFiveUsers = listOf {length=pure 5} genUserProfile
+```
+
+The `listOf` function takes a `length` generator (which we provide as a constant `5`), and creates a new recipe that runs the generator how a provided
+`length` generator generated times.
+
+Run it in the REPL:
+
+```bash
+echo -e ':exec printLn =<< pick1 genFiveUsers' |
+ rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr
+```
+
+The output will be a list of five unique, randomly-generated users:
+
+```text
+[MkProfile "Alice" 84, MkProfile "Charlie" 30, MkProfile "Bob" 41, MkProfile "Bob" 59, MkProfile "Bob" 67]
+```
+
+---
+
+## Next Steps
+
+You've mastered the basics. Where you go next depends on your needs:
+
+- **Want to handle types that might be empty?** Continue to [Handling Emptiness](t02-handling-emptiness.md) to learn about `Gen0`, `empty`, and `pick`.
+- **Ready to have `DepTyCheck` do the work for you?** Continue to [Automatic Generator Derivation](t04-automatic-generator-derivation.md) to learn about
+`deriveGen`.
diff --git a/docs/source/tutorials/t02-handling-emptiness.md b/docs/source/tutorials/t02-handling-emptiness.md
new file mode 100644
index 000000000..77fee1626
--- /dev/null
+++ b/docs/source/tutorials/t02-handling-emptiness.md
@@ -0,0 +1,187 @@
+# 2. Handling Emptiness: When a Type Has No Values
+
+In the [first tutorial](t01-generator-monad.md), we used `Gen1`, which is a guarantee—a promise—that a value can always be generated. This works
+perfectly for types like `Nat` or `String` that always have inhabitants.
+
+But what happens when a type might be **uninhabited** (have no values at all) under certain conditions?
+
+This is a common scenario in dependently-typed programming. A perfect example is `Fin n`, the type of natural numbers from `0` up to `n-1`.
+
+- `Fin 3` has three inhabitants: `0`, `1`, and `2`.
+- `Fin 1` has one inhabitant: `0`.
+- But what about `Fin 0`? It asks for a number in the range `0` to `-1`. There are no such numbers. This type is **uninhabited**.
+
+It is impossible to write a generator that produces a value of type `Fin 0`, because none exist. Our testing library must be able to handle this
+gracefully. In this tutorial, you will learn how to write safe generators for types that might be empty. You will build a correct generator for `Fin n`
+and see how to handle its results safely.
+
+## Prerequisites
+
+This tutorial assumes you have completed [Installation and First Steps](t00-installation-and-setup.md) and the first tutorial, ["The Generator
+Monad"](t01-generator-monad.md).
+
+---
+
+## Step 1: Discovering the Problem
+
+Let's start by trying to write a generator for `Fin n` using only the tools we know from the first tutorial.
+
+### Create a new file named `EmptyTutorial.idr`
+
+### Add the following code to it. We need to import `Data.Fin` along with our usual testing modules
+
+```idris
+import Test.DepTyCheck.Gen
+import Data.Fin
+import System.Random.Pure.StdGen
+```
+
+Now, **try to write a `Gen1` generator** for `Fin n`. We can handle the case where `n` is greater than zero, but the `Z` (zero) case presents a major
+problem.
+
+```idris
+-- This is an INTENTIONALLY INCORRECT generator to show the problem
+genFinIncorrect : (n : Nat) -> Gen1 (Fin n)
+genFinIncorrect (S k) = FS <$> genFinIncorrect k
+genFinIncorrect Z = ?wat -- What could we possibly write here?
+```
+
+We have a problem. In the `(S k)` case, we can walk all possible values of `Fin (S k)` and convert them to `Fin` to create a generator. But in the `Z`
+case, what can we do?
+
+The type is `Gen1 (Fin 0)`, but `Fin 0` has no values. We can't use `pure` because we don't have a value to give it. We're stuck.
+
+```{note}
+The `Gen0` emptiness flag indicates this generator might fail to produce a value. Use it for types that may not have inhabitants (like `Fin 0`).
+This is the problem `DepTyCheck` is designed to solve. We need a way to tell the system that a generator is _intentionally_ empty.
+```
+
+---
+
+## Step 2: Introducing `Gen0` and `empty`
+
+`DepTyCheck` provides two new tools to solve this exact problem:
+
+- **`Gen0 a`**: A type for a generator that _might_ produce a value of type `a`. Think of it as a "possibly empty" recipe.
+- **`empty`**: A specific generator of type `Gen0 a` that is _guaranteed_ to produce nothing. It's the recipe for an empty set.
+
+Let's use these to fix our incorrect generator.
+
+### Add the correct `genFin` generator to your `EmptyTutorial.idr` file
+
+```idris
+-- A correct, safe generator for Fin n
+genFin : (n : Nat) -> Gen0 (Fin n)
+genFin Z = empty
+genFin (S k) = FS <$> elements' (allFins k)
+```
+
+The changes are small but critical:
+
+- The return type is now `Gen0 (Fin n)`, which signals that the result may be empty.
+
+```{note}
+The `empty` generator fails immediately. Combined with `pick`, it lets you express "try A, and if it fails, try B" logic without explicit branching.
+```
+
+- In the `Z` case, we can now simply return `empty`. This correctly tells `DepTyCheck` that the recipe for `Fin 0` produces nothing.
+
+---
+
+## Step 3: Running a `Gen0` Generator
+
+Because a `Gen0` generator might not produce a value, we can't use `pick1` (which promises to return one value). Instead, we must use `pick`, which
+safely handles the possibility of emptiness.
+
+- `pick1 gen` returns `a`
+- `pick gen` returns `Maybe a`
+
+Let's see this in action.
+
+### Run `genFin` for both an inhabited case (`Fin 3`) and an empty case (`Fin 0`)
+
+```idris
+run : IO ()
+run = do
+ printLn !(pick (genFin 3))
+ printLn !(pick (genFin 0))
+```
+
+Run it
+
+```bash
+echo -e ':exec run' | rlwrap pack repl ./src/CustomGen.idr
+```
+
+You will see something like that:
+
+```text
+Just 2
+Nothing
+```
+
+First result will be a `Fin 3` value wrapped in a `Just`, because a value could be generated. But for the second we used `empty` in our definition for
+`genFin Z`, `DepTyCheck` knows this generator can't produce a value, and `pick` safely returns `Nothing`
+
+This is the core of safe, dependently-typed testing. The type system allows us to model that some generations are impossible, and the runner (`pick`)
+allows us to handle those cases gracefully at runtime without any crashes.
+
+## Step 4: Filtering with `suchThat`
+
+A type can also be effectively "empty" if we filter its values so much that none remain. `DepTyCheck` provides `suchThat` for this.
+
+I.e. `g` suchThat `p` takes a generator `g` and a predicate (a function that returns a `Bool`) `p`. It runs the generator `g`, and if the value it
+produces satisfies `p`, it returns it. If not, the generation fails for that attempt.
+
+Because the condition might never be met, `suchThat` always returns a `Gen0`.
+
+### Add these two generators to your `EmptyTutorial.idr` file
+
+```idris
+isEven : Nat -> Bool
+isEven n = n `mod` 2 == 0
+
+-- A generator that tries to find an even number between 0 and 10.
+-- This will sometimes succeed and sometimes fail (if `choose` picks an odd number).
+genEven : Gen0 Nat
+genEven = choose (0, 10) `suchThat` isEven
+
+-- A generator that tries to find a number greater than 10 in a range where none exist.
+-- This recipe is impossible and will always be empty.
+genImpossible : Gen0 Int
+genImpossible = choose (1, 10) `suchThat` (> 10)
+```
+
+### Run them both
+
+```idris
+runSuchThat : IO ()
+runSuchThat = do
+ printLn !(pick genEven)
+ printLn !(pick genImpossible)
+```
+
+Run it
+
+```bash
+echo -e ':exec runSuchThat' | rlwrap pack repl ./src/CustomGen.idr
+```
+
+You will see something like that:
+
+```text
+Just 2
+Nothing
+```
+
+This demonstrates another critical aspect of `Gen0`: it allows for speculative generation that might fail, giving you a powerful way to define complex
+properties.
+
+---
+
+## Next Steps
+
+Now that you've mastered manual generation for both simple and complex types, it's time to see how `DepTyCheck` can do this work for you automatically.
+
+- **Next Tutorial:** Continue to **[Measuring Your Test Coverage](t03-measuring-test-coverage.md)** to learn how to analyze the quality of your
+generated data.
diff --git a/docs/source/tutorials/t03-measuring-test-coverage.md b/docs/source/tutorials/t03-measuring-test-coverage.md
new file mode 100644
index 000000000..cbb014b10
--- /dev/null
+++ b/docs/source/tutorials/t03-measuring-test-coverage.md
@@ -0,0 +1,176 @@
+# 3. Measuring Your Test Coverage
+
+In the last tutorials, we learned how to write generators for random data. But how do we know if our random data is _good_? Are we testing all the
+important cases, or is our generator accidentally biased, leaving critical parts of our code untested?
+
+If a generator only ever produces one kind of value, our tests won't find bugs that only appear in other cases. We need a way to measure the quality of
+our random data.
+
+## Our Goal
+
+In this tutorial, you will learn how to add **labels** to your generators to measure your test coverage. You will build a generator for a `TrafficLight`
+data type, add labels to track each color, and run a test that produces a coverage report, like this:
+
+```text
+TrafficLight covered fully (1000 times)
+ - Red: covered (332 times)
+ - Green: covered (334 times)
+ - Amber: covered (334 times)
+```
+
+## Prerequisites
+
+This tutorial assumes you have completed [Installation and First Steps](t00-installation-and-setup.md) and the first two tutorials on [basic
+generation](t01-generator-monad.md) and [emptiness handling](t02-handling-emptiness.md).
+
+---
+
+## Step 1: Creating a Generator to Test
+
+First, let's create a simple data type and a generator for it. This will be the subject of our coverage analysis.
+
+### Create a new file named `CoverageTutorial.idr`
+
+```idris
+import Data.List
+import Data.List.Lazy
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+import System.Random.Pure.StdGen
+
+import Control.Monad.Maybe
+import Control.Monad.Random
+import Control.Monad.State
+```
+
+### Add the following code to it
+
+```idris
+data TrafficLight = Red | Amber | Green
+
+Show TrafficLight where
+ show Red = "Red"
+ show Amber = "Amber"
+ show Green = "Green"
+
+-- A generator that produces a traffic light color
+genTrafficLight : Gen1 TrafficLight
+genTrafficLight = oneOf [pure Red, pure Amber, pure Green]
+```
+
+This generator works, but we have no way of knowing if it's distributing its results evenly. To see that, we need to add labels.
+
+---
+
+## Step 2: Generating the Coverage Report
+
+To get a full, aggregated coverage report, we need to run the generator many times and combine the results. This is a three-step process:
+
+1. Initialize Report: Create an empty `CoverageGenInfo` report. This serves as a template that knows about all the types and constructors in our
+generator.
+2. Collect Data: Run the generator many times and collect the raw `ModelCoverage` (the label counts) from each individual run.
+3. Analyze Results: Fold the collected raw data into the report template to produce the final, printable `CoverageGenInfo`.
+
+```{note}
+Coverage measurement happens in three phases:
+
+1. Generate many samples with different random seeds
+2. Track which constructors appear
+3. Report how much every constructor had been called
+```
+
+Here is how to implement this in a `main` function.
+
+### Add a `main` function to your `CoverageTutorial.idr` file
+
+```idris
+runReportWithCoverage : IO ()
+runReportWithCoverage = do
+ -- Step 1: Initialize the report template.
+ let reportTemplate = initCoverageInfo genTrafficLight
+
+ -- Step 2: Run the generator 1000 times to collect raw coverage data.
+ -- `withCoverage` is needed here because our generator is written by hand.
+ let rawCoverageRuns = unGenTryND 1000 someStdGen (withCoverage genTrafficLight)
+ let allRawCoverage = concatMap fst rawCoverageRuns
+
+ -- Step 3: Fold the raw data into the template to get the final report.
+ let finalReport = registerCoverage allRawCoverage reportTemplate
+
+ -- 4. Print the final report.
+ putStrLn $ show finalReport
+```
+
+### Compile and run your file
+
+```bash
+idris2 --build CoverageTutorial.idr
+./build/exec/CoverageTutorial
+```
+
+### Check the output
+
+You will see the aggregated coverage report printed to your console. Because we used `oneOf`, the distribution should be very even:
+
+```text
+TrafficLight covered fully (1000 times)
+ - Red: covered (332 times)
+ - Green: covered (334 times)
+ - Amber: covered (334 times)
+```
+
+This gives us high confidence that our generator is testing all three `TrafficLight` cases equally.
+
+---
+
+## Step 3: Debugging with Labels
+
+Besides aggregated reports, labels are also an invaluable tool for debugging. You can instruct the generator runner to print every label as it's
+activated. This allows you to trace the execution of a single, complex generation.
+
+`DepTyCheck` uses the `CanManageLabels` interface to handle this. By default, the `pick` function we've used before uses the `IgnoreLabels`
+implementation. But we can provide a different one, `PrintAllLabels`, to change its behavior.
+
+### Add a new `runDebug` function to your file
+
+This new function will use `pick` and provide the `PrintAllLabels` implementation via the `@{}` syntax.
+
+```idris
+runDebug : IO ()
+runDebug = do
+ Just v <- runMaybeT {m=IO}
+ $ evalRandomT someStdGen
+ $ evalStateT Z $ unGen {labels = PrintAllLabels} (withCoverage genTrafficLight)
+ | Nothing => putStrLn "couldn't produce a value"
+ putStrLn $ "Generated withCoverage: " ++ show v
+
+ val <- pick genTrafficLight
+ putStrLn $ "Generated via pick: " ++ show val
+```
+
+### Compile and run the file again
+
+```bash
+ idris2 --build CoverageTutorial.idr
+ ./build/exec/CoverageTutorial
+```
+
+### Analyze the output. You will see a clear difference
+
+```text
+Main.TrafficLight[?]
+Main.Amber (user-defined)
+Generated withCoverage: Amber
+Generated via pick: Just Green
+```
+
+In the first run, the label was printed to the console the moment the corresponding generator was executed. In second run, no label were printed. For a
+deeply nested generator, this trace allows you to understand exactly which path was taken to produce a specific problematic value.
+
+---
+
+## Next Steps
+
+Now that you can write, run, and measure generators manually, it's time to learn how `DepTyCheck` can do all of this for you automatically.
+
+- **Next Tutorial:** Continue to **[Automatic Generator Derivation](t04-automatic-generator-derivation.md)** to learn how to use `deriveGen`.
diff --git a/docs/source/tutorials/t04-automatic-generator-derivation.md b/docs/source/tutorials/t04-automatic-generator-derivation.md
new file mode 100644
index 000000000..cd20fe491
--- /dev/null
+++ b/docs/source/tutorials/t04-automatic-generator-derivation.md
@@ -0,0 +1,275 @@
+# 4. Automatic Generator Derivation
+
+In the previous tutorials, we showed how to write generators by hand. This is fine for simple types, but quickly becomes tedious and error-prone for
+complex, recursive data structures.
+
+This is where `DepTyCheck` shines. It comes with a powerful macro, `deriveGen`, that inspects your data type at compile-time and automatically writes a
+high-quality generator for it, handling recursion and constraints for you.
+
+## Our Goal
+
+In this tutorial, we will use a single, running example—a file system `Entry`—to demonstrate the power of `deriveGen`. We will:
+
+1. Show how complex a manual generator for `Entry` would be.
+2. Replace it with a single `deriveGen` call.
+3. Learn how to provide an **external generator** to produce meaningful filenames.
+4. Learn how to **pass arguments** to the generator to make it context-aware.
+
+## Prerequisites
+
+- Completion of [Installation and First Steps](t00-installation-and-setup.md) and the tutorials on [manual generation](t01-generator-monad.md),
+[emptiness](t02-handling-emptiness.md), and [coverage analysis](t03-measuring-test-coverage.md).
+
+### Create a new file named `DeriveTutorial.idr`
+
+```idris
+import Deriving.DepTyCheck.Gen -- For the deriveGen macro
+import Data.Fuel
+
+import Test.DepTyCheck.Gen
+import System.Random.Pure.StdGen
+```
+
+We need the `%language ElabReflection` pragma to enable compile-time elaboration which will automatically write code for defined generators by their
+types.
+
+```idris
+%language ElabReflection
+```
+
+---
+
+## Step 1: The Burden of Manual Derivation
+
+Let's start with a recursive data type for a file system entry.
+
+```idris
+data EntryManual = FileManual String | DirectoryManual (List EntryManual)
+
+Show EntryManual where
+ show (FileManual s) = "FileManual " ++ show s
+ show (DirectoryManual l) = "DirectoryManual " ++ (assert_total $ show l)
+```
+
+How would we write a generator for this by hand? It would be complex:
+
+- We would need to accept a `Fuel` parameter to stop recursion.
+- In the `DirectoryManual` case, we'd need to call ourself with less fuel.
+- We'd have to balance the choice between `FileManual` and `DirectoryManual` to get a good distribution.
+- We would need a separate generator for the `String` in `FileManual`.
+
+A sketch might look like this:
+
+```idris
+-- A complex, manual generator (conceptual)
+genEntryManual : Fuel -> Gen MaybeEmpty EntryManual
+genEntryManual Dry = pure (FileManual "default.txt") -- Base case when out of fuel
+genEntryManual (More recFuel) =
+ frequency
+ [ (1, FileManual <$> elements ["file1", "file2"]) -- some string generator
+ , (1, DirectoryManual <$> (listOf (genEntryManual recFuel)) ) -- recursive call
+ ]
+ where
+```
+
+Prepare a test for it:
+
+```idris
+runEntryManual : IO ()
+runEntryManual = do
+ printLn "limit = 1"
+ for_ (the (List Int) [1..5]) $ \_ => do
+ Just e <- pick (genEntryManual (limit 1))
+ | Nothing => printLn "Generation failed"
+ printLn e
+
+ printLn "limit = 2"
+ for_ (the (List Int) [1..5]) $ \_ => do
+ Just e <- pick (genEntryManual (limit 2))
+ | Nothing => printLn "Generation failed"
+ printLn e
+
+ printLn "limit = 3"
+ for_ (the (List Int) [1..5]) $ \_ => do
+ Just e <- pick (genEntryManual (limit 3))
+ | Nothing => printLn "Generation failed"
+ printLn e
+```
+
+This is a lot of work to get right. Now, let's do it the easy way.
+
+---
+
+## Step 2: Automatic Derivation with `deriveGen`
+
+We can replace the manual logic with a single line. But it has some limitations. To make the automagic generation works we need to drop off polymorphic
+parameters:
+
+```idris
+mutual
+ data EntryList : Type where
+ Nil : EntryList
+ (::) : Entry -> EntryList -> EntryList
+
+ data Entry = File String | Directory EntryList
+
+mutual
+ Show Entry where
+ show (File s) = "File " ++ show s
+ show (Directory l) = "Directory " ++ (assert_total $ show l)
+
+ Show EntryList where
+ show xs = "[" ++ show' xs ++ "]" where
+ show' : EntryList -> String
+ show' Nil = ""
+ show' (x :: Nil) = show x
+ show' (x :: xs) = show x ++ ", " ++ show' xs
+```
+
+```{note}
+The latest version of DepTyCheck supports polymorphic specialization for automatically derived generators, but its support is still experimental. Also
+automagic generator deriving supports only `Gen MaybeEmpty` for now. If you need stricter `Gen NonEmpty`, you still need to do it by your hands.
+```
+
+### Define the generator
+
+Our first naive attempt to use `deriveGen` might be the following:
+
+```idris
+failing "Cannot derive generator for the primitive type String, use external instead"
+ genEntry : Fuel -> Gen MaybeEmpty Entry
+ genEntry = deriveGen
+```
+
+But honestly DepTyCheck is would decline our example because we need also to pass a generator for strings. It does not present out of the box, so, we
+need some to add some special stuff around which will be uncovered by further tutorials.
+
+```idris
+%hint
+genStr : Gen MaybeEmpty String
+genStr = elements ["a", "b", "c", "d", "f", "g", "h"]
+
+genEntry : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty Entry
+genEntry = deriveGen
+```
+
+That's it. The `deriveGen` macro will now inspect the `Entry` type and write a generator that handles recursion, fuel, choices, and even attaches a
+generator for `String` from the context. It might also automatically add the coverage labels we learned about in further tutorials!
+
+You can immediately generate a random file system structure.
+
+Prepare a test for it:
+
+```idris
+runEntryDefault : IO ()
+runEntryDefault = do
+ Just e <- pick (genEntry (limit 10))
+ | Nothing => printLn "Generation failed"
+ printLn e
+```
+
+Running this might produce output like: `Directory [File "a", Directory [File "b"]]`.
+
+---
+
+## Step 3: Providing an External Generator
+
+The default generator is powerful, but the `String`s it produces are random nonsense. To generate meaningful data, we can provide `deriveGen` with a
+"hint" in the form of an external generator.
+
+### Write a custom `String` generator
+
+This generator will produce realistic filenames.
+
+```idris
+genFilename : Fuel -> Gen MaybeEmpty String
+genFilename _ = elements ["config.yml", "main.idr", "README.md"]
+```
+
+### Call the new generator
+
+When we call `genEntry`, we can use the `@{...}` syntax to pass our `genFilename` function to satisfy the constraint.
+
+```idris
+runEntryWithHint : IO ()
+runEntryWithHint = do
+ putStrLn "--- Generating Entries with a custom String generator ---"
+ for_ (the (List Int) [1..5]) $ \_ => do
+ Just e <- pick (genEntry @{genFilename} (limit 5))
+ | Nothing => printLn "Generation failed"
+ printLn e
+```
+
+You will see that `deriveGen` still handles the `Directory` and `List` logic automatically, but every `File` now contains one of your hand-picked
+filenames.
+
+```text
+--- Generating Entries with a custom String generator ---
+Directory [File "main.idr"]
+File "config.yml"
+Directory []
+File "README.md"
+Directory [Directory [File "config.yml"]]
+```
+
+---
+
+## Step 4: Passing Runtime Arguments
+
+Sometimes, a generator needs more context than `Fuel`. For example, what if we want to generate files with names that are context-dependent, based on
+their parent directory?
+
+Any arguments that appear in the signature _before_ the `Fuel` parameter are treated as regular inputs. `deriveGen` is smart enough to thread these
+arguments through its recursive calls.
+
+### Write a context-aware `String` generator
+
+This generator takes a `path` prefix as an argument and changes its output accordingly.
+
+```idris
+genContextAwareFilename : String -> Fuel -> Gen MaybeEmpty String
+genContextAwareFilename path _ =
+ if path == "src"
+ then elements ["main.idr", "lib.idr"]
+ else if path == "doc"
+ then elements ["tutorial.md", "README.md"]
+ else elements ["file.txt"]
+```
+
+To call `genCtxEntry`, we provide the initial path, and our context-aware generator. The `deriveGen` engine will handle passing the `path` argument down
+to `genContextAwareFilename` during any recursive calls.
+
+Prepare a test for it:
+
+```idris
+runCtxEntry : IO ()
+runCtxEntry = do
+ putStrLn "--- Generating files in `src` directory ---"
+ -- We pass the initial path "src" and the context-aware generator
+ Just e <- pick (genEntry @{genContextAwareFilename "src"} (limit 5))
+ | Nothing => printLn "Generation Failed"
+ printLn e
+```
+
+You will see that files generated have names appropriate for the `src` directory, because our custom generator was called with `path = "src"`.
+
+```text
+--- Generating files in `src` directory ---
+Directory [Directory [], Directory [], File "main.idr", File "lib.idr"]
+```
+
+This powerful pattern allows you to create highly flexible generators that adapt their behavior based on runtime context.
+
+---
+
+## Next Steps
+
+Now that you know how to automatically generate data and provide hints, you are ready for more advanced topics:
+
+- **Want to learn how to control what gets generated?** Continue to **[DeriveGen Signatures](t05-derivegen-signatures.md)** to learn how to use given vs
+generated parameters and dependent pairs in signatures.
+- **Want to understand how recursion affects generation?** Continue to **[Beyond Fuel](t07-beyond-fuel.md)** to learn about `SpendingFuel` vs
+`StructurallyDecreasing` recursion.
+- **How do I fix a biased generator or control generation order?** The default derivation strategy is smart, but sometimes needs more specific guidance.
+Continue to **[Derivation Tuning](t10-derivation-tuning.md)** to learn how to use `instance` declarations to control constructor probabilities and
+argument generation order.
diff --git a/docs/source/tutorials/t05-derivegen-signatures.md b/docs/source/tutorials/t05-derivegen-signatures.md
new file mode 100644
index 000000000..b9499e04a
--- /dev/null
+++ b/docs/source/tutorials/t05-derivegen-signatures.md
@@ -0,0 +1,202 @@
+# 5. DeriveGen Signatures: Controlling What Gets Generated
+
+In the previous tutorial, we saw how `deriveGen` can automatically create generators. But how do we tell it _what kind_ of data we want? For example,
+should the length of a `Vect` be given as an argument, or should it be randomly generated?
+
+The answer is the function signature. The signature is not just a type; it is a blueprint of your intent that tells `deriveGen` exactly what to do.
+
+## Our Goal
+
+In this tutorial, we will learn to command `deriveGen` by writing three different function signatures for the `Vect` type. By the end of this tutorial,
+you will have built:
+
+1. A generator for a `Vect` of a **specific, given** length.
+2. A generator that produces a `Vect` of a **random, generated** length.
+3. A flexible generator that takes both a **given** length and an **external generator** for its elements.
+
+This will give you a deep understanding of how to use signatures to control `deriveGen`.
+
+## Prerequisites
+
+- All previous tutorials, especially [Measuring Your Test Coverage](t03-measuring-test-coverage.md).
+
+---
+
+## Step 1: The Setup
+
+First, let's create our file and add the necessary imports. We will be using `Vect` throughout this tutorial.
+
+### Create a new file named `DeriveTutorial.idr`
+
+### Add the following boilerplate
+
+This includes the `ElabReflection` pragma and all the modules we will need.
+
+```idris
+import Deriving.DepTyCheck.Gen
+import Data.Vect
+import Data.Fuel
+
+import Test.DepTyCheck.Gen
+import System.Random.Pure.StdGen
+
+%language ElabReflection
+
+%hint
+genStr : Fuel -> Gen MaybeEmpty String
+genStr _ = elements ["a", "b", "c", "d", "f", "g", "h"]
+
+public export
+data VectString : (len : Nat) -> Type where
+ Nil : VectString Z
+ (::) : (x : String) -> (xs : VectString len) -> VectString (S len)
+
+Show (VectString n) where
+ show xs = "[" ++ show' xs ++ "]" where
+ show' : forall n . VectString n -> String
+ show' Nil = ""
+ show' (x :: Nil) = show x
+ show' (x :: xs) = show x ++ ", " ++ show' xs
+```
+
+---
+
+_Note: For the following steps, you can put all the code in the same `DeriveTutorial.idr` file and temporarily rename the `main` function you want to
+run as `main` before compiling._
+
+## Step 2: Scenario A - Generating a `Vect` of a Given Length
+
+Our first goal is to create a generator that produces a `Vect` of a specific length that we provide as an argument. To do this, we simply place the
+argument _before_ the `Fuel` parameter in the signature.
+
+The signature `(n : Nat) -> Fuel -> Gen MaybeEmpty (Vect n String)` tells `deriveGen`: "You will be _given_ a `Nat` named `n`. Your job is to produce a
+`Vect` of that exact length."
+
+Define the generator:
+
+```idris
+genVectOfLen : Fuel -> (n : Nat) -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty (VectString n)
+genVectOfLen = deriveGen
+```
+
+Let's write a `main` function to call our generator, providing `5` as the length.
+
+```idris
+runVect : IO ()
+runVect = do
+ putStrLn "--- Generating a Vect of a given length (5) ---"
+ Just v <- pick (genVectOfLen (limit 10) 5)
+ | Nothing => printLn "Generation failed"
+ printLn v
+```
+
+The output will show a `Vect` that always has exactly 5 elements, filled with random strings from the default `String` generator.
+
+Compile and run:
+
+```text
+--- Generating a Vect of a given length (5) ---
+["a", "b", "c", "d", "e"]
+The length is: 5
+```
+
+By placing `n` before `Fuel`, you have successfully commanded `deriveGen` to use it as a fixed input.
+
+---
+
+## Step 3: Scenario B - Generating a `Vect` of a Random Length
+
+What if we don't want to provide a specific length? What if we want the generator itself to invent a random length? To do this, we use a **dependent
+pair** in the return type.
+
+The signature `Fuel -> Gen MaybeEmpty (n ** Vect n String)` tells `deriveGen`: "Your job is to first generate a random `Nat` (which you will call `n`),
+and then generate a `Vect` of that length. When you are done, give me back both `n` and the `Vect`."
+
+Define the generator:
+
+```idris
+genRandomVect : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty (n ** VectString n)
+genRandomVect = deriveGen
+```
+
+This time, when we call the generator, we don't provide a length. The generator will produce a pair containing the length it chose and the vector it
+created.
+
+Prepare a test for it:
+
+```idris
+runRandomVect : IO ()
+runRandomVect = do
+ putStrLn "--- Generating a Vect of a random length ---"
+ for_ (the (List Int) [1..3]) $ \_ => do
+ Just (n ** v) <- pick (genRandomVect (limit 10))
+ | Nothing => printLn "Generation failed"
+ printLn n
+ printLn v
+```
+
+You will see vectors of different, random lengths each time you run it.
+
+Compile and run:
+
+```text
+--- Generating a Vect of a random length ---
+3
+["a", "b", "c"]
+0
+[]
+5
+["d", "e", "f", "g", "h"]
+```
+
+By moving the parameter `n` from an input to a **generated** part of the output using the `**` syntax, you have completely changed `deriveGen`'s
+behavior.
+
+---
+
+## Step 4: The Flexible Generator - Combining Patterns
+
+Let's combine the patterns we've learned. Our first generator is flexible enough: it is taking a `Nat` as a _given_ input, but it is also taking an
+_external generator_ hint for the element type using the `=>` syntax which will be overridden by the following exapmple.
+
+To call this generator, we must provide both the length `n` and an element generator via the `@` syntax.
+
+Prepare a test for it:
+
+```idris
+runFlexi : IO ()
+runFlexi = do
+ putStrLn "--- Generating a Vect of length 7 with overridden Str generator ---"
+ let myStrGen = \fuel => elements ["A", "B", "C"] -- Our custom generator for the elements
+ -- It is created manually, so no need to use `fuel`.
+
+ Just v <- pick (genVectOfLen (limit 10) 7 @{myStrGen})
+ | Nothing => printLn "Generation failed"
+ printLn v
+
+ Just v' <- pick (genVectOfLen (limit 10) 7 @{genStr})
+ | Nothing => printLn "Generation failed"
+ printLn v'
+```
+
+### Compile, run, and observe
+
+You will see a `Vect` of length 7, filled with numbers between 100 and 200, proving that `deriveGen` correctly used both your given length and your
+external generator.
+
+```text
+--- Generating a Vect of length 7 with overridden Str generator ---
+["A", "C", "B", "A", "A", "A", "C"]
+["b", "c", "f", "a", "b", "b", "h"]
+```
+
+---
+
+## Next Steps
+
+Now that you know how to control `deriveGen` through signatures, you are ready for more advanced topics:
+
+- **Want to understand how recursion affects generation?** Continue to **[Beyond Fuel: Structural Recursion](t07-beyond-fuel.md)** to learn about
+`SpendingFuel` vs `StructurallyDecreasing` recursion.
+- **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](t08-generating-gadts-with-proofs.md)** to see how
+`deriveGen` handles types like `SortedList`.
diff --git a/docs/source/tutorials/t06-mixing-manual-and-automatic.md b/docs/source/tutorials/t06-mixing-manual-and-automatic.md
new file mode 100644
index 000000000..f41685f4a
--- /dev/null
+++ b/docs/source/tutorials/t06-mixing-manual-and-automatic.md
@@ -0,0 +1,170 @@
+# 6. Mixing Manual and Automatic Generation
+
+In the [previous tutorial](t05-derivegen-signatures.md), we saw how to control what `deriveGen` generates by crafting function signatures. We also saw
+how to give it "hints" for primitive types like `String` using the `=>` syntax.
+
+But what if you have a custom data type that needs a special, handwritten generator? `DepTyCheck` provides a powerful, "magic" feature: if you define a
+generator for a type, `deriveGen` will automatically find it and use it.
+
+## Our Goal
+
+In this tutorial, you will:
+
+1. Define a custom type with a handwritten generator
+2. Mark that generator with `%hint` for automatic discovery
+3. See `deriveGen` automatically find and use your generator without explicit passing
+4. Compare implicit (`%hint`) vs explicit (`@{...}`) generator passing
+
+You will see output like:
+
+```text
+--- Testing mixed generation ---
+MkUser (MkSpecialString "root") 5
+```
+
+---
+
+## Prerequisites
+
+- Completion of [Tutorial 5: DeriveGen Signatures](t05-derivegen-signatures.md)
+- Understanding of the `=>` syntax for explicit generator constraints
+- Idris2 source file `./src/Mixed.idr` with the header:
+
+```idris
+import Test.DepTyCheck.Gen
+import Data.Fuel
+import Deriving.DepTyCheck.Gen
+import System.Random.Pure.StdGen
+
+%language ElabReflection
+```
+
+---
+
+## Step 1: Define Types and a Handwritten Generator
+
+Imagine we have a `SpecialString` type that should only ever contain specific, predefined values (e.g., usernames with special privileges). A fully
+random `String` generator is not appropriate here.
+
+### Create a new file named `Mixed.idr`
+
+### Define the `SpecialString` type with a `%hint` generator
+
+```idris
+-- A type that needs special generation
+data SpecialString = MkSpecialString String
+
+Show SpecialString where
+ show (MkSpecialString s) = "MkSpecialString " ++ show s
+
+-- A handwritten generator for SpecialString
+%hint
+genSpecialString : Gen MaybeEmpty SpecialString
+genSpecialString = map MkSpecialString (elements ["admin", "root", "system"])
+```
+
+### Define the `User` type that contains `SpecialString`
+
+```idris
+-- Standard domain types
+data User = MkUser SpecialString Nat
+
+Show User where
+ show (MkUser s i) = "MkUser (" ++ show s ++ ") " ++ show i
+```
+
+- Signature `Gen MaybeEmpty SpecialString` (no `Fuel ->`) is used for manually defined generators
+- The `%hint` pragma marks `genSpecialString` for **auto-implicit search** in Idris 2. It makes this function a candidate for automatic insertion - no
+explicit `@{genSpecialString}` required!
+
+```{note}
+From Idris 2 docs: `%hint` marks functions for auto search, similar to unnamed type class instances. The compiler prioritizes these hints during
+unification when explicit arguments are absent.
+```
+
+---
+
+## Step 2: Create the Derived Generator
+
+Now, let's define a generator for `User` using `deriveGen`. A `User` contains a `SpecialString` and a `Nat`. `deriveGen` knows how to generate a `Nat`
+by default. What will it do for `SpecialString`?
+
+### Add the derived generator to `Mixed.idr`
+
+```idris
+-- Add deriveGen for the User
+genUser : Fuel -> (Fuel -> Gen MaybeEmpty SpecialString) => Gen MaybeEmpty User
+genUser = deriveGen
+```
+
+- Automatic derivation by `deriveGen` requires `Fuel ->`
+- The constraint `(Fuel -> Gen MaybeEmpty SpecialString) =>` tells `deriveGen` it needs a generator for `SpecialString`
+
+```{note}
+Normally, you'd pass it explicitly: `genUser @{genSpecialString} fuel`. But `%hint` enables automatic resolution - Idris finds and inserts
+`genSpecialString` automatically!
+```
+
+---
+
+## Step 3: Test the Generator
+
+Let's create a main function to see our automatic discovery in action.
+
+### Add a test function to `Mixed.idr`
+
+```idris
+main : IO ()
+main = do
+ putStrLn "--- Testing mixed generation ---"
+ Just u <- pick (genUser (limit 10))
+ | Nothing => putStrLn "Generation failed"
+ printLn u
+```
+
+### Compile and run
+
+```bash
+pack build Mixed && pack exec Mixed
+```
+
+Expected output (will vary):
+
+```text
+--- Testing mixed generation ---
+MkUser (MkSpecialString "root") 5
+```
+
+---
+
+## When to Use %hint?
+
+`Constraint + %hint` approach is recommended for custom types.
+
+**Pattern:** Mark your generator with `%hint`, add constraint to derived generator:
+
+ ```idris
+ %hint
+ genMyType : Gen MaybeEmpty MyType
+ genMyType = map MkMyType (elements ["a", "b"])
+
+ genContainer : Fuel -> (Gen MaybeEmpty MyType) => Gen MaybeEmpty Container
+ genContainer = deriveGen
+ ```
+
+**Call site:**
+
+ ```idris
+ pick (genContainer fuel) -- No @{...} needed!
+ ```
+
+**Best for:** Custom types where you want automatic discovery with explicit dependencies in the signature.
+
+---
+
+## Next Steps
+
+- **Continue to the next tutorial:** [Generating GADTs with Proofs](t08-generating-gadts-with-proofs.md) to see how these techniques apply to even more
+advanced types with proof constraints.
+- **Experiment:** Try creating your own custom type with a `%hint` generator and see if `deriveGen` finds it automatically.
+- **Read more:** Check out the Idris 2 documentation on `%hint` for advanced auto-implicit search patterns.
diff --git a/docs/source/tutorials/t07-beyond-fuel.md b/docs/source/tutorials/t07-beyond-fuel.md
new file mode 100644
index 000000000..0faff4116
--- /dev/null
+++ b/docs/source/tutorials/t07-beyond-fuel.md
@@ -0,0 +1,236 @@
+# 7. Beyond Fuel: A Tutorial on Structural Recursion
+
+In our previous tutorials, we learned that `Fuel` is a crucial safety mechanism. It provides a "generation budget" that prevents `deriveGen` from
+getting stuck in an infinite loop when generating recursive data.
+
+For a simple type like `List`, the rule is easy to understand: every `Cons` call is a recursive step, so it must spend one unit of fuel. But is this
+always the case? Is every recursive call equally "expensive"?
+
+## Our Goal
+
+In this tutorial, you will discover that `deriveGen` is smart enough to identify two different kinds of recursion, with very different performance
+characteristics. You will write two generators:
+
+1. A generator for a Peano `Nat` type that strictly obeys the fuel budget.
+2. A generator for the indexed `Fin` type that appears to get "free" recursion, defying the budget.
+
+You will learn why this happens, how to recognize the difference between **`SpendingFuel`** and **`StructurallyDecreasing`** recursion, and how you can
+design your own types to take advantage of this powerful optimization.
+
+## Prerequisites
+
+- All previous tutorials, especially [Automatic Generator Derivation](t04-automatic-generator-derivation.md).
+
+---
+
+## Step 1: The Standard Case - `SpendingFuel` Recursion
+
+Let's start by examining the type of recursion we are already familiar with. We will create a simple Peano number type, where `deriveGen` must spend
+fuel on every recursive call to guarantee termination.
+
+### Create a new file named `RecursionTutorial.idr`
+
+```idris
+import Deriving.DepTyCheck.Gen
+import Data.Fuel
+import Data.Fin
+
+import Test.DepTyCheck.Gen
+import System.Random.Pure.StdGen
+
+%language ElabReflection
+```
+
+### Add the following code
+
+This defines our `PNat` (Peano Natural) type and a standard derived generator for it.
+
+```idris
+data PNat = PZ | PS PNat
+
+Show PNat where
+ show n = show (the Integer (pnatToInteger n))
+ where
+ pnatToInteger : PNat -> Integer
+ pnatToInteger PZ = 0
+ pnatToInteger (PS k) = 1 + pnatToInteger k
+
+genPNat : Fuel -> Gen MaybeEmpty PNat
+genPNat = deriveGen
+```
+
+### The Experiment
+
+Now, let's write a `main` function to call this generator twice: once with a generous fuel budget (`limit 10`) and once with a very small one (`limit
+3`).
+
+```idris
+runPeano : IO ()
+runPeano = do
+ putStrLn "--- Generating with a large fuel budget (10) ---"
+ Just p_large <- pick (genPNat (limit 10))
+ | Nothing => printLn "Generation failed"
+ printLn p_large
+
+ putStrLn "--- Generating with a small fuel budget (3) ---"
+ Just p_small <- pick (genPNat (limit 3))
+ | Nothing => printLn "Generation failed"
+ printLn p_small
+```
+
+### Compile, run, and observe
+
+```bash
+idris2 --build RecursionTutorial.idr
+./build/exec/RecursionTutorial
+```
+
+Your output will be random, but it will follow a strict pattern:
+
+```text
+--- Generating with a large fuel budget (10) ---
+PS (PS (PS (PS (PS PZ))))
+--- Generating with a small fuel budget (3) ---
+PS (PS PZ)
+```
+
+Notice that the generator with more fuel produced a larger number. The number of `PS` constructors is strictly limited by the fuel you provide. This is
+because `deriveGen` identifies the `PS` constructor as `SpendingFuel`. For each `PS` it generates, it must consume one unit of fuel from the budget.
+This is the default, safe behavior for simple recursive types.
+
+---
+
+## Step 2: StructurallyDecreasing Recursion
+
+Must `deriveGen` _always_ spend fuel on recursion? No. If it can prove that a recursive call is guaranteed to terminate by its structure alone, it can
+perform a powerful optimization.
+
+A perfect example is `Fin n`, the type of numbers from `0` to `n-1`.
+
+### Add the `Fin` generator to your `RecursionTutorial.idr` file
+
+```idris
+genFin : Fuel -> (n : Nat) -> Gen MaybeEmpty (Fin n)
+genFin = deriveGen
+```
+
+### The Counter-Intuitive Experiment
+
+Now, let's try to generate a `Fin 100`. This would require 100 recursive calls to `FS`. According to our last experiment, this should require at least
+`limit 100` fuel. But what happens if we only give it `limit 3`?
+
+```idris
+runFin : IO ()
+runFin = do
+ putStrLn "--- Generating a large Fin with a tiny fuel budget (3) ---"
+ -- We ask for a Fin up to 100, but only provide fuel for 3 steps!
+ Just fin <- pick (genFin (limit 3) 100)
+ | Nothing => printLn "Generation failed"
+ printLn fin
+```
+
+### Run the experiment and observe the surprising result
+
+```text
+ --- Generating a large Fin with a tiny fuel budget (3) ---
+ 97
+```
+
+It works! Even with a tiny fuel budget, it successfully generated a very large `Fin` value. It did not fail or run out of fuel.
+
+### The Explanation
+
+This is not magic. `deriveGen` is smart enough to analyze the `Fin` type and its `FS` constructor
+
+`FS : Fin k -> Fin (S k)`
+
+It sees that the input `Fin k` is for a type whose index `k` is provably, _structurally smaller_ than the output's index `S k`. Because the `Nat` index
+itself guarantees that the recursion will eventually terminate when it hits `Fin 0`, `deriveGen` does not need to use the `Fuel` parameter as a safety
+budget. It classifies this kind of recursion as `StructurallyDecreasing`.
+
+This optimization allows `deriveGen` to generate values for indexed, recursive data types like `Fin` and `Vect` much more efficiently than it can for
+simple recursive types like `PNat` or `List`.
+
+---
+
+## Under the Hood: How deriveGen Uses Fuel
+
+### The Mental Model
+
+`deriveGen` generates code that follows a simple pattern: a `case` split on the `Fuel` parameter.
+
+```text
+genSomething : Fuel -> Gen MaybeEmpty Something
+genSomething Dry = -- Base case: no fuel, choose non-recursive constructors
+genSomething (More f) = -- Recursive case: spend fuel or use optimization
+```
+
+- When `Fuel` is `Dry`, the generator **must** choose non-recursive constructors (like `PZ`, `Leaf`, `Nil`)
+- When `Fuel` is `More f`, the generator **can** choose recursive constructors (like `PS`, `Node`, `Cons`)
+- Each recursive call consumes one unit of `Fuel` (calls with `f` instead of `More f`)
+- This guarantees termination: eventually `Fuel` reaches `Dry` and recursion stops
+
+This is why higher `Fuel` values produce larger structures — more recursive steps are allowed before hitting the `Dry` base case.
+
+But the key insight is: **deriveGen doesn't always spend fuel on recursion**. It depends on the type of recursion.
+
+### SpendingFuel: Manual Implementation
+
+For a type like `PNat`, the generated code looks like this:
+
+```idris
+genPNat' : Fuel -> Gen MaybeEmpty PNat
+genPNat' Dry = pure PZ -- Must choose non-recursive constructor
+genPNat' (More f) = frequency
+ [ (1, pure PZ) -- Non-recursive option
+ , (1, PS <$> genPNat' f) -- Recursive: spends fuel (calls with f, not More f)
+ ]
+```
+
+```{note}
+When generating `PS`, we call `genPNat' f` — we pass the **smaller** fuel value. Each recursive step consumes one unit of fuel.
+```
+
+### StructurallyDecreasing: Manual Implementation
+
+For `Fin`, the generated code would be different:
+
+```idris
+genFin' : (n : Nat) -> Fuel -> Gen MaybeEmpty (Fin n)
+genFin' Z _ = empty -- No values for Fin 0
+genFin' (S k) fuel = frequency
+ [ (1, pure FZ) -- Base constructor
+ , (1, FS <$> genFin' k fuel) ] -- Recursive: SAME fuel!
+```
+
+```{note}
+When generating `FS`, we call `genFin' k fuel` — with the **same** fuel value!
+```
+
+Why is this safe? Because the **type index** decreases (`S k` → `k`), guaranteeing termination even without
+spending fuel. The index itself acts as the termination measure.
+
+### The Key Difference
+
+| Aspect | SpendingFuel | StructurallyDecreasing |
+| -------- | -------------- | ------------------------ |
+| **Fuel in recursive call** | `gen f` (less fuel) | `gen fuel` (same fuel) |
+| **Termination proof** | Fuel budget decreases | Type index decreases |
+| **Max generated size** | Limited by fuel | Limited by index |
+| **Examples** | `PNat`, `List a`, `Tree` | `Fin n`, `Vect n a` |
+
+This is the core optimization: when the type system guarantees termination through decreasing indices, `deriveGen` doesn't need to spend fuel. This
+makes generation of indexed types both faster and capable of producing larger values.
+
+---
+
+## Next Steps
+
+Now that you understand how `deriveGen` handles recursion, you are ready for more advanced topics:
+
+- **Want to fix biased generators?** Continue to **[Derivation Tuning](t10-derivation-tuning.md)** to learn how to use `ProbabilityTuning` and
+`GenOrderTuning` instances.
+- **Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](t06-mixing-manual-and-automatic.md)** to see how
+`deriveGen` discovers and uses your custom generators.
+- **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](t08-generating-gadts-with-proofs.md)** to see how
+`deriveGen` handles auto-implicit proof arguments.
diff --git a/docs/source/tutorials/t08-generating-gadts-with-proofs.md b/docs/source/tutorials/t08-generating-gadts-with-proofs.md
new file mode 100644
index 000000000..ecf0accd0
--- /dev/null
+++ b/docs/source/tutorials/t08-generating-gadts-with-proofs.md
@@ -0,0 +1,240 @@
+# 8. Generating GADTs with Proof Constraints
+
+In previous tutorials, we used `deriveGen` for regular data types and indexed types like `Vect`. But what about types that carry **proofs** as
+constructors arguments? Can `deriveGen` handle those?
+
+Yes! `deriveGen` is smart enough to automatically satisfy proof constraints during generation.
+
+## Our Goal
+
+In this tutorial, you will build a generator for a `SortedList` type that is **always sorted by construction**. The type itself carries a proof of
+sortedness, and `deriveGen` will automatically find valid values that satisfy the proof constraints.
+
+By the end, you will:
+
+1. Define a GADT with a proof argument (`{auto prf : isSorted ...}`)
+2. Derive a generator with a single `deriveGen` call
+3. Run the generator and verify that all output is sorted
+
+## Prerequisites
+
+- Completion of [Tutorial 5: DeriveGen Signatures](t05-derivegen-signatures.md)
+- Understanding of dependent pairs and indexed types
+- Idris2 source file `./src/Playground.idr` with the header:
+
+```idris
+import Deriving.DepTyCheck.Gen
+import System.Random.Pure.StdGen
+```
+
+## Step 1: Define a SortedList Type
+
+First, let's define a list type that is guaranteed to be sorted. The key is that the `SCons` constructor requires a proof that adding a new element
+maintains sortedness.
+
+```idris
+isSorted : List Nat -> Bool
+isSorted [] = True
+isSorted [_] = True
+isSorted (x :: y :: xs) = x <= y && isSorted (y :: xs)
+
+mutual
+ data SortedList : Type where
+ SNil : SortedList
+ SCons : (x : Nat) -> (xs : SortedList) -> {auto prf : So $ isSorted (x :: toList xs)} -> SortedList
+
+ toList : SortedList -> List Nat
+ toList SNil = []
+ toList (SCons x xs) = x :: toList xs
+```
+
+The `SCons` constructor has an **auto-implicit** argument `{auto prf : isSorted (x :: toList xs)}`. This means:
+
+- To construct an `SCons`, Idris must find a proof that the list is sorted.
+- The `auto` keyword tells Idris to search for this proof automatically.
+
+```{note}
+The `{auto prf : isSorted ...}` constraint ensures only sorted lists are generated. The `auto` keyword makes Idris search for proof automatically
+during generation.
+```
+
+---
+
+## Step 2: Derive the Generator
+
+Now comes the magic. We derive a generator for `SortedList` with a single line.
+
+### Add the derived generator
+
+```idris
+genSortedList : Fuel -> Gen MaybeEmpty SortedList
+genSortedList = deriveGen
+```
+
+That's it! No manual logic, no special handling for the proof argument. `deriveGen` will:
+
+1. Generate a candidate `x : Nat`
+2. Recursively generate `xs : SortedList`
+3. Check if `isSorted (x :: toList xs)` can be proven
+4. If yes, construct the `SCons`; if no, try another `x`
+
+---
+
+## Step 3: Run and Verify
+
+Let's test the generator and verify that all output is sorted.
+
+```idris
+testList : HasIO io => io ()
+testList = do
+ putStrLn "--- Generating 5 sorted lists ---"
+ for_ (the (List Int) [1..5]) $ \_ => do
+ Just sl <- pick (genSortedList (limit 5))
+ | Nothing => printLn "Generation failed"
+ let asList = toList sl
+ putStrLn $ "Generated: " ++ show asList
+ putStrLn $ "Is sorted: " ++ show (isSorted asList)
+```
+
+### Compile and run
+
+```bash
+echo -e ':exec testList' | rlwrap pack repl ./src/Playground.idr
+```
+
+### Analyze the output
+
+```text
+...
+Main> --- Generating 5 sorted lists ---
+Generated: [2, 3, 3, 4, 4]
+Is sorted: True
+Generated: [2, 2]
+Is sorted: True
+Generated: [3, 4]
+Is sorted: True
+Generated: [2]
+Is sorted: True
+Generated: [4]
+Is sorted: True
+```
+
+Every generated list is sorted! `deriveGen` automatically found values of `x` that satisfy the `isSorted` constraint.
+
+---
+
+## Step 4: Understanding How It Works
+
+How does `deriveGen` solve the proof constraint? The key is in the **search order** and **backtracking**.
+
+When `deriveGen` encounters `{auto prf : So $ isSorted (x :: toList xs)}`, it:
+
+1. **Generates candidates** for `x` from the default `Nat` generator
+2. **Recursively generates** `xs : SortedList` (which is already sorted by construction)
+3. **Checks the constraint**: Is `x <= head xs` (or `x` can be anything if `xs` is empty)?
+4. **Backtracks if needed**: If the constraint fails, it tries another `x`
+
+```{note}
+The proof argument guarantees sortedness by construction:
+
+- `SNil` is always sorted (base case)
+- `SCons` requires proof that new element maintains order
+- Invalid constructions are rejected at compile time
+```
+
+This is why the generator may be slower for complex constraints — it may need multiple attempts to find valid values.
+
+The `Fuel` parameter controls how deep the recursion can go, so, with more fuel, `deriveGen` can generate longer sorted lists:
+
+```idris
+-- Add to main:
+testFuel : IO ()
+testFuel = do
+ putStrLn "\n--- With small fuel (limit 3) ---"
+ Just sl1 <- pick (genSortedList (limit 3))
+ | Nothing => printLn "Generation failed"
+ printLn $ toList sl1
+
+ putStrLn "\n--- With large fuel (limit 8) ---"
+ Just sl2 <- pick (genSortedList (limit 8))
+ | Nothing => printLn "Generation failed"
+ printLn $ toList sl2
+```
+
+Run it:
+
+```bash
+echo -e ':exec testFuel' | rlwrap pack repl ./src/Playground.idr
+...
+Main> --- Generating 5 sorted lists ---
+Generated: [2, 3, 3, 4, 4]
+Is sorted: True
+Generated: [2, 2]
+Is sorted: True
+Generated: [3, 4]
+Is sorted: True
+Generated: [2]
+Is sorted: True
+Generated: [4]
+Is sorted: True
+```
+
+---
+
+## Step 5: Another Example — Bounded Values
+
+Let's see another example of proof-carrying data. Consider a type that represents numbers bounded by a given limit:
+
+```idris
+data BoundedNat : (limit' : Nat) -> Type where
+ MkBounded : (n : Nat) -> {auto prf : n `LT` limit'} -> BoundedNat limit'
+
+genBoundedNat : Fuel -> (limit' : Nat) -> Gen MaybeEmpty (BoundedNat limit')
+genBoundedNat = deriveGen
+
+testBounded : IO ()
+testBounded = do
+ putStrLn "--- Generating BoundedNat with limit'=5 ---"
+ for_ (the (List Int) [1..5]) $ \_ => do
+ Just bn <- pick (genBoundedNat (limit 10) 5)
+ | Nothing => printLn "Failed"
+ case bn of
+ MkBounded n => putStrLn $ "Generated: " ++ show n ++ " (< 5)"
+```
+
+Run it:
+
+```bash
+echo -e ':exec testBounded' | rlwrap pack repl ./src/Playground.idr
+```
+
+The output might be varied:
+
+```text
+Main> --- Generating BoundedNat with limit'=5 ---
+Generated: 4 (< 5)
+Generated: 1 (< 5)
+Generated: 1 (< 5)
+Generated: 3 (< 5)
+Generated: 4 (< 5)
+```
+
+The `{auto prf : LT n limit}` constraint ensures that only values less than the limit are generated. `deriveGen` will automatically search for valid `n`
+values.
+
+---
+
+## Next Steps
+
+Now that you can generate proof-carrying data, you are ready for more advanced topics:
+
+- **Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](t06-mixing-manual-and-automatic.md)** to see how
+`deriveGen` automatically discovers and uses your custom generators.
+
+
diff --git a/docs/source/tutorials/t09-toy-example.md b/docs/source/tutorials/t09-toy-example.md
new file mode 100644
index 000000000..7dc1274b7
--- /dev/null
+++ b/docs/source/tutorials/t09-toy-example.md
@@ -0,0 +1,341 @@
+# 9. Toy Example: Generating ASTs for a DSL
+
+In previous tutorials, we learned how to create generators for simple data types and how to combine manual and automatic derivation. Now, let's apply
+these skills to a real-world scenario: generating **Abstract Syntax Trees (ASTs)** for a simple imperative programming language.
+
+This tutorial is based on **PIL (Primitive Imperative Language)**, a real example from the DepTyCheck repository.
+
+## Our Goal
+
+In this tutorial, you will build a complete AST generator for a simple imperative language. By the end, you will have:
+
+1. Defined expression and statement types for the language
+2. Created both automatic (`deriveGen`) and hand-written generators
+3. Generated valid random programs with control flow structures
+
+You will see output like:
+
+```text
+Seq (Assign "x" (Lit 5)) (If (Add (Var "x") (Lit 3)) (Assign "y" (Lit 10)) Skip)
+```
+
+**Expected time:** 30-40 minutes
+
+---
+
+## Step 1: Define the Expression Language
+
+Let's start with the foundation: arithmetic and logical expressions.
+
+### Create a new file named `PILTutorial.idr`
+
+### Add the basic setup and expression type
+
+```idris
+import Data.Fuel
+import Data.List
+import Deriving.DepTyCheck.Gen
+import Test.DepTyCheck.Gen
+import System.Random.Pure.StdGen
+
+-- Arithmetic and logical expressions
+data Expr : Type where
+ Lit : Nat -> Expr
+ Var : String -> Expr
+ Add : Expr -> Expr -> Expr
+ Mul : Expr -> Expr -> Expr
+ And : Expr -> Expr -> Expr
+ Lt : Expr -> Expr -> Expr
+
+Show Expr where
+ show (Lit l) = "Lit " ++ show l
+ show (Var s) = "Var " ++ show s
+ show (Add e1 e2) = "Add (" ++ show e1 ++ ") (" ++ show e2 ++ ")"
+ show (Mul e1 e2) = "Mul (" ++ show e1 ++ ") (" ++ show e2 ++ ")"
+ show (And e1 e2) = "And (" ++ show e1 ++ ") (" ++ show e2 ++ ")"
+ show (Lt e1 e2) = "Lt (" ++ show e1 ++ ") (" ++ show e2 ++ ")"
+```
+
+### Create a simple derived generator with a generator-helper for strings
+
+```idris
+genVarName : Fuel -> Gen MaybeEmpty String
+genVarName _ = elements ["x", "y", "z", "temp", "result", "counter"]
+
+genExpr : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty Expr
+genExpr = deriveGen
+```
+
+### Test it
+
+```idris
+main : IO ()
+main = do
+ putStrLn "--- Generating random expressions ---"
+ for_ (the (List Int) [1..5]) $ \_ => do
+ Just e <- pick (genExpr @{genVarName} (limit 3))
+ | Nothing => putStrLn "Generation failed"
+ printLn e
+```
+
+### Build and run
+
+```bash
+echo -e ':exec main' | rlwrap pack repl ./PILTutorial.idr
+```
+
+Expected output (will vary):
+
+```text
+--- Generating random expressions ---
+Lt (Mul (Lt (Var "x") (Var "temp")) (Add (Lit 3) (Lit 1))) (Add (Var "temp") (Lt (Var "result") (Lit 0)))
+Lt (And (Var "counter") (And (Lit 2) (Var "y"))) (And (Lit 1) (Add (Lit 0) (Var "counter")))
+And (Mul (And (Lit 0) (Lit 0)) (Lit 3)) (Lit 3)
+Mul (Lit 2) (Var "z")
+Add (Lit 0) (Add (And (Var "y") (Lit 2)) (And (Lit 2) (Var "counter")))
+```
+
+```{note}
+`deriveGen` automatically handles the recursive structure of expressions. The `limit 3` fuel controls the maximum depth of nested expressions.
+```
+
+---
+
+## Step 2: Add Statements and Control Flow
+
+Now let's add statements that form complete programs.
+
+### Add the statement type to your file
+
+```idris
+-- Statements with control flow
+data Stmt : Type where
+ Skip : Stmt
+ Assign : String -> Expr -> Stmt
+ Seq : Stmt -> Stmt -> Stmt
+ If : Expr -> Stmt -> Stmt -> Stmt
+ While : Expr -> Stmt -> Stmt
+
+Show Stmt where
+ show Skip = "Skip"
+ show (Assign s e) = "Assign " ++ show s ++ " (" ++ show e ++ ")"
+ show (Seq s1 s2) = "Seq (" ++ show s1 ++ ") (" ++ show s2 ++ ")"
+ show (If e1 s1 s2) = "If (" ++ show e1 ++ ") (" ++ show s1 ++ ") (" ++ show s2 ++ ")"
+ show (While e1 s1) = "While (" ++ show e1 ++ ") (" ++ show s1 ++ ")"
+```
+
+### Create a hand-written generator with explicit fuel control
+
+```idris
+genStmt : Fuel -> Gen MaybeEmpty Stmt
+genStmt Dry = pure Skip -- Base case: only non-recursive constructors
+genStmt (More f) = frequency
+ [ (1, pure Skip)
+ , (5, Assign <$> genVarName (More f) <*> genExpr @{genVarName} (More f))
+ , (3, Seq <$> genStmt f <*> genStmt f)
+ , (2, If <$> genExpr @{genVarName} (More f) <*> genStmt f <*> genStmt f)
+ , (2, While <$> genExpr @{genVarName} (More f) <*> genStmt f)
+ ]
+```
+
+```{note}
+- `genStmt Dry = pure Skip` ensures termination when fuel is exhausted
+- `genStmt f` (less fuel) in recursive calls controls program size
+- `frequency` weights make simple statements more common than complex ones
+```
+
+### Test the statement generator
+
+```idris
+main_stmt : IO ()
+main_stmt = do
+ putStrLn "--- Generating random statements ---"
+ for_ (the (List Int) [1..5]) $ \_ => do
+ Just s <- pick (genStmt (limit 4))
+ | Nothing => putStrLn "Generation failed"
+ printLn s
+```
+
+Try to run `main_stmt`
+
+```bash
+echo -e ':exec main_stmt' | rlwrap pack repl ./PILTutorial.idr
+```
+
+Expected output:
+
+```text
+--- Generating random statements ---
+Assign "counter" (Lt (Lit 0) (Lit 4))
+Assign "x" (Lt (Mul (Lt (Var "temp") (Lit 1)) (Lit 2)) (Lt (Var "counter") (And (Add (Var "y") (Lit 2)) (And (Var "counter") (Lit 2)))))
+Assign "y" (And (Add (Mul (Var "x") (Var "temp")) (Var "temp")) (And (Mul (Mul (Var "y") (Lit 3)) (Lt (Var "counter") (Lit 2))) (Var "result")))
+If (Lt (Mul (And (Lt (Lit 4) (Var "z")) (Add (Lit 1) (Var "x")))
+ (Mul (Mul (Var "x") (Var "y")) (Add (Lit 0) (Lit 0))))
+ (And (Lt (Add (Lit 3) (Lit 0)) (Mul (Lit 0) (Var "counter")))
+ (Add (Var "z") (Var "temp")))
+ (Assign "counter" (And (Mul (And (Var "z") (Lit 1)) (Var "result")) (Var "result")))
+ (If (Lt (Mul (And (Var "z") (Var "counter")) (Lit 0))
+ (Add (Lit 0) (Mul (Lit 3) (Lit 3))))
+ (If (Mul (Mul (Lit 0) (Var "result")) (And (Lit 1) (Var "temp")))
+ (While (Lt (Var "x") (Var "y")) (Skip))
+ (While (Lt (Var "result") (Var "temp")) (Skip)))
+ (Assign "temp" (Lt (Mul (Lit 2) (Lit 1)) (Mul (Lit 0) (Var "counter")))))
+Seq (Assign "result" (Var "z"))
+ (While (Add (Add (Var "counter") (And (Lit 3) (Lit 2)))
+ (Lt (And (Var "temp") (Lit 1)) (Var "temp")))
+ (Assign "y" (And (Lt (Var "counter") (Lit 1))
+ (Lt (Var "counter") (Var "temp")))))
+```
+
+---
+
+## Step 3: Generate Complete Programs
+
+Now let's generate complete programs with multiple statements.
+
+### Define a Program type and generator
+
+```idris
+-- A program is a list of statements
+data Program = MkProgram (List Stmt)
+
+Show Program where
+ show (MkProgram lst) = "MkProgram " ++ show lst
+
+genProgram : (n : Nat) -> Fuel -> Gen MaybeEmpty Program
+genProgram n fuel = MkProgram <$> listOf {length=pure n} (genStmt fuel)
+```
+
+### Test program generation
+
+```idris
+main_program : IO ()
+main_program = do
+ putStrLn "--- Generating a random program (5 statements) ---"
+ Just prog <- pick (genProgram 5 (limit 3))
+ | Nothing => putStrLn "Generation failed"
+ printLn prog
+```
+
+Try to run
+
+```bash
+echo -e ':exec main_program' | rlwrap pack repl ./PILTutorial.idr
+```
+
+Expected output:
+
+```text
+--- Generating a random program (5 statements) ---
+MkProgram [Seq (While (Add (Lit 1) (And (Lit 1) (Var "x"))) (While (Var "x") (Skip)))
+ (Assign "temp" (And (And (Var "temp") (Var "y")) (Lit 1))),
+ If (And (Add (Add (Var "x") (Lit 0)) (Lit 1)) (Lit 2))
+ (Assign "result" (Lt (Lt (Lit 2) (Var "temp")) (Mul (Var "y") (Var "y"))))
+ (While (Var "temp") (Seq (Skip) (Skip))),
+ While (Mul (Var "result") (Mul (Lit 1) (Add (Var "y") (Lit 1))))
+ (Assign "counter" (Lt (And (Lit 1) (Var "result")) (Lit 0))),
+ Seq (If (And (And (Lit 1) (Var "result")) (Mul (Lit 0) (Lit 1)))
+ (If (Lit 1) (Skip) (Skip)) (While (Lit 0) (Skip)))
+ (If (Mul (Add (Var "x") (Lit 1)) (And (Lit 1) (Var "counter")))
+ (While (Add (Lit 1) (Lit 1)) (Skip))
+ (Assign "y" (Add (Lit 1) (Lit 0)))),
+ Assign "temp" (Add (Add (Lit 1) (And (Var "y") (Var "z"))) (And (Lit 1) (Lit 3)))]
+```
+
+```{note}
+`listOf {length=pure n} gen` runs the generator `n` times and collects results into a list.
+```
+
+---
+
+## Step 4: Test Properties of Generated Programs
+
+Let's verify that our generated programs have certain properties.
+
+### Add property checking functions
+
+```idris
+-- Check if a statement contains an assignment
+hasAssign : Stmt -> Bool
+hasAssign Skip = False
+hasAssign (Assign _ _) = True
+hasAssign (Seq s1 s2) = hasAssign s1 || hasAssign s2
+hasAssign (If _ s1 s2) = hasAssign s1 || hasAssign s2
+hasAssign (While _ s) = hasAssign s
+
+-- Count statements in a program
+stmtCount : Program -> Nat
+stmtCount (MkProgram stmts) = length stmts
+
+-- Check if program has a loop
+hasLoop : Stmt -> Bool
+hasLoop Skip = False
+hasLoop (Assign _ _) = False
+hasLoop (Seq s1 s2) = hasLoop s1 || hasLoop s2
+hasLoop (If _ s1 s2) = hasLoop s1 || hasLoop s2
+hasLoop (While _ _) = True
+```
+
+### Test properties
+
+```idris
+main_properties : IO ()
+main_properties = do
+ putStrLn "--- Checking properties of generated programs ---"
+ for_ (the (List Int) [1..10]) $ \_ => do
+ Just prog <- pick (genProgram 3 (limit 3))
+ | Nothing => putStrLn "Generation failed"
+
+ let hasAnyAssign = Prelude.any {t=List} hasAssign (case prog of MkProgram stmts => stmts)
+ let hasAnyLoop = Prelude.any {t=List} hasLoop (case prog of MkProgram stmts => stmts)
+ let count = stmtCount prog
+
+ putStrLn $ "Program with " ++ show count ++ " statements"
+ putStrLn $ " Has assignment: " ++ show hasAnyAssign
+ putStrLn $ " Has loop: " ++ show hasAnyLoop
+ putStrLn ""
+```
+
+Try to run
+
+```bash
+echo -e ':exec main_properties' | rlwrap pack repl ./PILTutorial.idr
+```
+
+A sample of the output:
+
+```text
+--- Checking properties of generated programs ---
+Program with 3 statements
+ Has assignment: True
+ Has loop: False
+
+Program with 3 statements
+ Has assignment: True
+ Has loop: True
+
+Program with 3 statements
+ Has assignment: True
+ Has loop: False
+...
+```
+
+```{note}
+You can use these property checks to ensure your generated programs meet certain criteria for testing compilers or interpreters.
+```
+
+---
+
+## Next Steps
+
+Now that you can generate complex ASTs, you're ready for many other applications:
+
+- **Test an interpreter:** Use your generated PIL programs to test a language interpreter with property-based testing.
+- **Add more language features:** Extend the language with functions, arrays, or I/O operations.
+- **Integrate custom generators:** Continue to **[Mixing Manual and Automatic](t06-mixing-manual-and-automatic.md)** to see how `deriveGen` discovers
+and uses your custom generators.
+- **Control distribution:** Continue to **[Derivation Tuning](t10-derivation-tuning.md)** to learn how to fine-tune constructor probabilities for more
+realistic program distributions.
+
+The complete `PILTutorial.idr` file is available for reference. You can find it in the DepTyCheck examples or build it step-by-step following this
+tutorial.
diff --git a/docs/source/tutorials/t10-derivation-tuning.md b/docs/source/tutorials/t10-derivation-tuning.md
new file mode 100644
index 000000000..05612fd32
--- /dev/null
+++ b/docs/source/tutorials/t10-derivation-tuning.md
@@ -0,0 +1,211 @@
+# 10. Advanced Derivation Tuning
+
+In the last tutorial, we saw how to use `deriveGen` and provide it with custom generators for base types like `String`. However, `DepTyCheck` offers
+even deeper, more powerful mechanisms for controlling the derivation process for situations where just providing a generator isn't enough.
+
+```{warning}
+**This is an Advanced Tutorial.** The tuning mechanism uses some of Idris's more powerful features, specifically compile-time reflection
+and type class instances. We will walk through it step-by-step, but a full explanation of these concepts is beyond the scope of this tutorial. If you
+just want to use `deriveGen` with its default settings and provide external generators, you can safely skip this lesson.
+```
+
+## Our Goal
+
+We will tackle two common problems that cannot be solved with external generators alone:
+
+1. Fixing Bias: We will prove that a default generator is biased and then implement the `ProbabilityTuning` interface to change the frequency of a
+specific constructor.
+2. Fixing Inefficiency: We will show how a naive generator for a constrained type is inefficient and then implement the `GenOrderTuning` interface to
+guide the derivation logic and make it robust.
+
+## Prerequisites
+
+- Completion of [Automatic Generator Derivation](t04-automatic-generator-derivation.md).
+- A willingness to engage with some advanced Idris concepts!
+
+---
+
+## Step 1: Discovering a Biased Generator
+
+Let's start by defining a simple, recursive data type where the default `deriveGen` strategy will produce a biased result.
+
+### Create a new file named `TuningTutorial.idr`
+
+```idris
+import Deriving.DepTyCheck.Gen
+import Deriving.DepTyCheck.Gen.Tuning -- For the tuning interfaces
+import Data.Fuel
+import Data.So
+
+-- From previous tutorials
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+import System.Random.Pure.StdGen
+
+%language ElabReflection
+
+%hint
+genStr : Gen MaybeEmpty String
+genStr = elements ["a", "b", "c", "d", "f", "g", "h"]
+```
+
+### Add the following code
+
+```idris
+mutual
+ data EntryList : Type where
+ Nil : EntryList
+ (::) : Entry -> EntryList -> EntryList
+
+ data Entry = File String | Directory EntryList
+
+-- A generator for Entry that takes an external String generator
+genEntry : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty Entry
+genEntry = deriveGen
+```
+
+### Add a coverage analysis `main` function
+
+```idris
+main : IO ()
+main = do
+ let reportTemplate = initCoverageInfo genEntry
+ let rawCoverageRuns = unGenTryND 1000 someStdGen (genEntry (limit 10))
+ let allRawCoverage = concatMap fst rawCoverageRuns
+ let finalReport = registerCoverage allRawCoverage reportTemplate
+ putStrLn $ show finalReport
+```
+
+### Analyze the report
+
+The results will be starkly imbalanced because `deriveGen` prefers the non-recursive `File` constructor
+
+```text
+ Entry covered fully (1000 times)
+ - File: covered (909 times)
+ - Directory: covered (91 times)
+```
+
+This is the problem we need to solve.
+
+---
+
+## Step 2: Probability Tuning
+
+To fix the bias, we must implement the `ProbabilityTuning` interface for the `Directory` constructor. This tells `deriveGen` to override its default
+weight.
+
+### Define the implementation
+
+Place this implementation at the top level of your file. It targets the `Directory` constructor by its name
+
+```idris
+mutual
+ data EntryListP : Type where
+ Nil2 : EntryListP
+ Q2 : EntryP -> EntryListP -> EntryListP
+
+ data EntryP = FileP String | DirectoryP EntryListP
+
+-- A generator for Entry that takes an external String generator
+genEntryP : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty EntryListP
+genEntryP = deriveGen
+
+ProbabilityTuning `{DirectoryP}.dataCon where
+ isConstructor = itIsConstructor
+ tuneWeight _ = 1
+```
+
+- `ProbabilityTuning ... where`: We define a specific implementation of this interface for a constructor.
+- `"Directory".dataCon`: This is a `Name` literal that refers to the `Directory` constructor. Since `Directory` is defined in this same file, we can use
+the simple name without a module prefix.
+- `isConstructor = itIsConstructor`: This is a required line of reflection boilerplate that confirms we have targeted a valid constructor.
+- `tuneWeight _ = 10`: We implement the `tuneWeight` function. It takes the default weight `_` and we ignore it, always returning our new, higher weight
+of `10`.
+
+### Re-run the coverage analysis
+
+The compiler will now automatically find and apply our implementation. Simply recompile and run.
+
+```idris
+mainP : IO ()
+mainP = do
+ let reportTemplate = initCoverageInfo genEntryP
+ let rawCoverageRuns = unGenTryND 1000 someStdGen (genEntryP (limit 10))
+ let allRawCoverage = concatMap fst rawCoverageRuns
+ let finalReport = registerCoverage allRawCoverage reportTemplate
+ putStrLn $ show finalReport
+```
+
+### Analyze the new report
+
+The distribution will now be much closer to a 50/50 balance, proving we have successfully tuned the probability.
+
+```text
+ Entry covered fully (1000 times)
+ - File: covered (526 times)
+ - Directory: covered (474 times)
+```
+
+---
+
+## Step 3: Generation Order Tuning
+
+Probability isn't the only thing we can tune. For some dependent types, the _order_ in which arguments are generated is critical for efficiency.
+Consider a pair `(n, m)` where we require `n < m`.
+
+```idris
+data LtPair : Type where
+ MkLtPair : (n : Nat) -> (m : Nat) -> (prf : So $ n < m) -> LtPair
+```
+
+`deriveGen`'s default strategy might randomly pick `n=10` and `m=5`, then fail because it can't prove `10 < 5`. This is very inefficient. We can tell it
+to generate `m` first, making it much easier to pick a valid `n`.
+
+### Define the generator and the tuning implementation in your file
+
+```idris
+GenOrderTuning `{MkLtPair}.dataCon where
+ isConstructor = itIsConstructor
+ deriveFirst _ _ = [`{m}]
+
+genLtPair : Fuel -> Gen MaybeEmpty LtPair
+genLtPair = deriveGen
+
+Show LtPair where
+ show (MkLtPair n m _) = "MkLtPair " ++ show n ++ " " ++ show m ++ " _"
+```
+
+- `GenOrderTuning ... where`: We implement the ordering interface for the `MkLtPair` constructor.
+- `deriveFirst _ _ = [``{m}]`: We implement `deriveFirst` to return a list of arguments that must be generated first. Here, we specify the argument
+named `m` using a name literal ```{m}`.
+
+### Test It
+
+With this instance in scope, `deriveGen` will now follow our instructions. When generating an `LtPair`, it will generate `m` first, and then be smart
+enough to only generate values for `n` that are less than `m`.
+
+```idris
+-- A main function to test the LtPair generator
+main_lt : IO ()
+main_lt = do
+ let reportTemplate = initCoverageInfo genLtPair
+ let rawCoverageRuns = unGenTryND 1000 someStdGen (genLtPair (limit 10))
+ let allRawCoverage = concatMap fst rawCoverageRuns
+ let finalReport = registerCoverage allRawCoverage reportTemplate
+ putStrLn $ show finalReport
+```
+
+You will see that this generator efficiently produces valid pairs like `MkLtPair 5 10 True` every time, without the wasteful failures of the naive
+approach.
+
+---
+
+## Next Steps
+
+- **Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](t06-mixing-manual-and-automatic.md)** to see how
+`deriveGen` automatically discovers and uses your custom generators.
+- **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](t08-generating-gadts-with-proofs.md)** to see how
+`deriveGen` handles GADTs with auto-implicit proof arguments.
+- **Want to see a complete example?** Continue to **[Toy Example: Generating ASTs for a DSL](t09-toy-example.md)** to build a complete generator for a
+simple imperative language.
diff --git a/docs/source/tutorials/test-function.md b/docs/source/tutorials/test-function.md
deleted file mode 100644
index 5343f3b89..000000000
--- a/docs/source/tutorials/test-function.md
+++ /dev/null
@@ -1 +0,0 @@
-# Test you first function
diff --git a/pack.toml b/pack.toml
index 9aab81d2a..17797f273 100644
--- a/pack.toml
+++ b/pack.toml
@@ -3,7 +3,12 @@
################
[install]
-whitelist = [ "deptycheck-docs", "pil-fun", "pil-dyn" ]
+whitelist = [ "deptycheck-docs"
+ , "pil-fun"
+ , "pil-dyn"
+ , "super-linter-run"
+ , "super-linter-fix"
+ ]
#######################
### Elab-util-extra ###
@@ -30,6 +35,16 @@ type = "local"
path = "docs"
ipkg = "docs.ipkg"
+[custom.all.super-linter-run]
+type = "local"
+path = ".linters"
+ipkg = "super-linter-run.ipkg"
+
+[custom.all.super-linter-fix]
+type = "local"
+path = ".linters"
+ipkg = "super-linter-fix.ipkg"
+
################
### Examples ###
################
diff --git a/tests/docs/typecheck/expected b/tests/docs/typecheck/expected
index fe4f238df..fa24eaf61 100644
--- a/tests/docs/typecheck/expected
+++ b/tests/docs/typecheck/expected
@@ -1,19 +1,27 @@
- 1/19: Building Tutorials.TestFunction (src/Tutorials/TestFunction.md)
- 2/19: Building Tutorials.Generators (src/Tutorials/Generators.md)
- 3/19: Building Tutorials.Derivation (src/Tutorials/Derivation.md)
- 4/19: Building Reference.Users.Pbt (src/Reference/Users/Pbt.md)
- 5/19: Building Reference.Users.GenMonad (src/Reference/Users/GenMonad.md)
- 6/19: Building Reference.Users.Derivation (src/Reference/Users/Derivation.md)
- 7/19: Building Reference.Contributors.GenMonad (src/Reference/Contributors/GenMonad.md)
- 8/19: Building Reference.Contributors.Derivation (src/Reference/Contributors/Derivation.md)
- 9/19: Building Meta.Test (src/Meta/Test.md)
-10/19: Building Explanation.Specifications.Recommendations (src/Explanation/Specifications/Recommendations.md)
-11/19: Building Explanation.Specifications.Experiments (src/Explanation/Specifications/Experiments.md)
-12/19: Building Explanation.Generators.Design (src/Explanation/Generators/Design.md)
-13/19: Building Explanation.Derivation.Design (src/Explanation/Derivation/Design.md)
-14/19: Building Explanation.Derivation.Design.WhenDerivationHappens (src/Explanation/Derivation/Design/WhenDerivationHappens.md)
-15/19: Building Explanation.Derivation.Design.TypeParamsAndIndices (src/Explanation/Derivation/Design/TypeParamsAndIndices.md)
-16/19: Building Explanation.Derivation.Design.SingleGen (src/Explanation/Derivation/Design/SingleGen.md)
-17/19: Building Explanation.Derivation.Design.SingleCon (src/Explanation/Derivation/Design/SingleCon.md)
-18/19: Building Explanation.Derivation.Design.DerivationTask (src/Explanation/Derivation/Design/DerivationTask.md)
-19/19: Building Explanation.Derivation.Design.ClosureOfGens (src/Explanation/Derivation/Design/ClosureOfGens.md)
+ 1/27: Building Tutorials.T10DerivationTuning (src/Tutorials/T10DerivationTuning.md)
+ 2/27: Building Tutorials.T09ToyExample (src/Tutorials/T09ToyExample.md)
+ 3/27: Building Tutorials.T08GeneratingGadtsWithProofs (src/Tutorials/T08GeneratingGadtsWithProofs.md)
+ 4/27: Building Tutorials.T07BeyondFuel (src/Tutorials/T07BeyondFuel.md)
+ 5/27: Building Tutorials.T06MixingManualAndAutomatic (src/Tutorials/T06MixingManualAndAutomatic.md)
+ 6/27: Building Tutorials.T05DerivegenSignatures (src/Tutorials/T05DerivegenSignatures.md)
+ 7/27: Building Tutorials.T04AutomaticGeneratorDerivation (src/Tutorials/T04AutomaticGeneratorDerivation.md)
+ 8/27: Building Tutorials.T03MeasuringTestCoverage (src/Tutorials/T03MeasuringTestCoverage.md)
+ 9/27: Building Tutorials.T02HandlingEmptiness (src/Tutorials/T02HandlingEmptiness.md)
+10/27: Building Tutorials.T01GeneratorMonad (src/Tutorials/T01GeneratorMonad.md)
+11/27: Building Tutorials.T00InstallationAndSetup (src/Tutorials/T00InstallationAndSetup.md)
+12/27: Building Reference.Users.Pbt (src/Reference/Users/Pbt.md)
+13/27: Building Reference.Users.GenMonad (src/Reference/Users/GenMonad.md)
+14/27: Building Reference.Users.Derivation (src/Reference/Users/Derivation.md)
+15/27: Building Reference.Contributors.GenMonad (src/Reference/Contributors/GenMonad.md)
+16/27: Building Reference.Contributors.Derivation (src/Reference/Contributors/Derivation.md)
+17/27: Building Meta.Test (src/Meta/Test.md)
+18/27: Building Explanation.Specifications.Recommendations (src/Explanation/Specifications/Recommendations.md)
+19/27: Building Explanation.Specifications.Experiments (src/Explanation/Specifications/Experiments.md)
+20/27: Building Explanation.Generators.Design (src/Explanation/Generators/Design.md)
+21/27: Building Explanation.Derivation.Design (src/Explanation/Derivation/Design.md)
+22/27: Building Explanation.Derivation.Design.WhenDerivationHappens (src/Explanation/Derivation/Design/WhenDerivationHappens.md)
+23/27: Building Explanation.Derivation.Design.TypeParamsAndIndices (src/Explanation/Derivation/Design/TypeParamsAndIndices.md)
+24/27: Building Explanation.Derivation.Design.SingleGen (src/Explanation/Derivation/Design/SingleGen.md)
+25/27: Building Explanation.Derivation.Design.SingleCon (src/Explanation/Derivation/Design/SingleCon.md)
+26/27: Building Explanation.Derivation.Design.DerivationTask (src/Explanation/Derivation/Design/DerivationTask.md)
+27/27: Building Explanation.Derivation.Design.ClosureOfGens (src/Explanation/Derivation/Design/ClosureOfGens.md)
diff --git a/tests/docs/typecheck/run b/tests/docs/typecheck/run
index 06e8b74f2..80befb361 100755
--- a/tests/docs/typecheck/run
+++ b/tests/docs/typecheck/run
@@ -9,28 +9,47 @@ DOCSDIR=../../../docs/source/
# Generate `src` dir and symlinks to all `*.md` files (upper-case renamed)
all_modules=$(
find "$DOCSDIR" -type f -name '*.md' -print | sort | while read r; do
- # capitalization idea taken from https://stackoverflow.com/questions/27703739/capitalize-words-in-a-bash-variable-using-sed
- capname=$(echo "${r#$DOCSDIR}" | sed 's/^./\u&/; s|/\(.\)|/\u\1|g; s/-\(.\)/\u\1/g')
+ # Use perl for cross-platform compatibility (MacOS BSD sed doesn't support \u)
+ # Convert explanation/derivation/design/closure-of-gens.md -> Explanation/Derivation/Design/ClosureOfGens.md
+ if command -v perl >/dev/null 2>&1; then
+ # Perl command explanation:
+ # s/(^|\/)(.)/\1\u\2/g - Capitalize letter at start (^) or after slash (/)
+ # s/-(.)/\u\1/g - Remove dash and capitalize following letter
+ capname=$(echo "${r#$DOCSDIR}" | perl -pe 's/(^|\/)(.)/\1\u\2/g; s/-(.)/\u\1/g')
+ else
+ # Sed command explanation (POSIX):
+ # s/^./\u&/ - Capitalize first character of string
+ # s|/\(.\)|/\u\1|g - Capitalize character after each slash
+ # s/-\(.\)/\u\1/g - Capitalize character after each dash
+ # On BSD/macOS sed, \u is literal 'u', producing uexplanation.uderivation...
+ # capitalization idea taken from https://stackoverflow.com/questions/27703739/capitalize-words-in-a-bash-variable-using-sed
+ capname=$(echo "${r#$DOCSDIR}" | sed 's/^./\u&/; s|/\(.\)|/\u\1|g; s/-\(.\)/\u\1/g')
+ fi
localname="src/$capname"
localdir=$(dirname "$localname")/
mkdir -p "$localdir"
+ # sed 's|[^/]*/|\.\./|g' replaces each directory component with ../
+ # Example: src/Explanation/Derivation/Design/ -> ../../../../
ln -s "$(echo "$localdir" | sed 's|[^/]*/|\.\./|g')$r" "$localname"
+ # Convert path to module name: remove .md extension, replace / with .
+ # Example: Explanation/Derivation/Design/ClosureOfGens.md -> Explanation.Derivation.Design.ClosureOfGens
modulename=$(echo "${capname%.md}" | sed 's|/|\.|g')
- echo -n ", $modulename"
+ # Use printf instead of echo -n for POSIX compliance and consistent behavior across shells
+ # printf outputs format string with variables, no trailing newline
+ printf ", %s" "$modulename" # Accumulate module names for docs.ipkg
done
)
-# Generate `docs.ipkg` containing all `*.md` files (upper-case renamed)
-[ -n "$all_modules" ] && echo \
-"
+# Use cat with heredoc instead of echo for reliable newline handling and escape sequences
+[ -n "$all_modules" ] && cat > docs.ipkg < docs.ipkg
+sourcedir = "src"
+EOF
# Build the docs
if [ -e docs.ipkg ]; then