[ docs ] Update note for tutorials, remove useless index

Author: GulinSS

docs/source/tutorials.rst

@@ -14,7 +14,6 @@ You can read more in the `original framework <https://diataxis.fr/tutorials/>`_
   :maxdepth: 1
   :caption: Choose what to learn
 
-  tutorials/index
   tutorials/t00-installation-and-setup
   tutorials/t01-generator-monad
   tutorials/t02-handling-emptiness
@@ -25,5 +24,10 @@ You can read more in the `original framework <https://diataxis.fr/tutorials/>`_
   tutorials/t07-beyond-fuel
   tutorials/t08-generating-gadts-with-proofs
   tutorials/t09-toy-example
+
+.. toctree::
+  :maxdepth: 1
+  :caption: Enjoy your curiosity
+
   tutorials/t10-derivation-tuning
   tutorials/t11-under-the-hood-a-derivegen-like-macro

docs/source/tutorials/index.md

@@ -38,8 +38,9 @@ Expected output:
 0.8.x
 ```
 
-> [!NOTE]\
-> You need Idris 2 version **0.8.0 or newer** for DepTyCheck to work.
+```{note}
+You need Idris 2 version **0.8.0 or newer** for DepTyCheck to work.
+```
 
 ---
 
@@ -59,8 +60,9 @@ pack update-db
 pack install deptycheck
 ```
 
-> [!NOTE]\
-> This command downloads and builds DepTyCheck. It may take a few minutes the first time.
+```{note}
+This command downloads and builds DepTyCheck. It may take a few minutes the first time.
+```
 
 ---
 
@@ -88,8 +90,9 @@ modules = Main
 depends = deptycheck
 ```
 
-> [!NOTE]\
-> The `depends = deptycheck` line tells Idris to use the DepTyCheck library.
+```{note}
+The `depends = deptycheck` line tells Idris to use the DepTyCheck library.
+```
 
 ---
 
@@ -118,11 +121,11 @@ main = do
   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
+```{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
+```
 
 ---
 
@@ -134,13 +137,6 @@ main = do
 pack build tutorial
 ```
 
-Expected output:
-
-```text
-Building tutorial...
-Build succeeded
-```
-
 ### Run the executable
 
 ```bash
@@ -153,8 +149,9 @@ Expected output (your result will vary):
 Yellow
 ```
 
-> [!NOTE]\
-> Run the command multiple times to see different results (Yellow, Green, Red).
+```{note}
+Run the command multiple times to see different results (Yellow, Green, Red).
+```
 
 ---
 

docs/source/tutorials/t00-installation-and-setup.md

@@ -53,9 +53,10 @@ 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.
+```{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
 
@@ -105,9 +106,10 @@ 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
+```{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"`).
 

docs/source/tutorials/t01-generator-monad.md

@@ -51,9 +51,10 @@ 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`).
+```{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.
+```
 
 ---
 
@@ -79,8 +80,9 @@ 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.
+```{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.
 

docs/source/tutorials/t02-handling-emptiness.md

@@ -71,12 +71,13 @@ 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
+```{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.
 

docs/source/tutorials/t03-measuring-test-coverage.md

@@ -126,10 +126,10 @@ mutual
       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
+```{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
 

docs/source/tutorials/t04-automatic-generator-derivation.md

@@ -73,14 +73,14 @@ Show User where
   show (MkUser s i) = "MkUser (" ++ show s ++ ") " ++ show i
 ```
 
-> [!NOTE]\
->
-> - 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
+- 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.
+```
 
 ---
 
@@ -97,12 +97,13 @@ genUser : Fuel -> (Fuel -> Gen MaybeEmpty SpecialString) => Gen MaybeEmpty User
 genUser = deriveGen
 ```
 
-> [!NOTE]\
->
-> - Automatic derivation by `deriveGen` requires `Fuel ->`
-> - The constraint `(Fuel -> Gen MaybeEmpty SpecialString) =>` tells `deriveGen` it needs a generator for `SpecialString`
-> - Normally, you'd pass it explicitly: `genUser @{genSpecialString} fuel`. But `%hint` enables automatic resolution - Idris finds and inserts
+- 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!
+```
 
 ---
 

docs/source/tutorials/t06-mixing-manual-and-automatic.md

@@ -187,9 +187,9 @@ genPNat' (More f) = frequency
   ]
 ```
 
-> [!NOTE]
->
-> When generating `PS`, we call `genPNat' f` — we pass the **smaller** fuel value. Each recursive step consumes one unit of fuel.
+```{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
 
@@ -203,9 +203,9 @@ genFin' (S k) fuel = frequency
   , (1, FS <$> genFin' k fuel) ]   -- Recursive: SAME fuel!
 ```
 
-> [!NOTE]
->
-> When generating `FS`, we call `genFin' k fuel` — with the **same** fuel value!
+```{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.

docs/source/tutorials/t07-beyond-fuel.md

@@ -53,9 +53,10 @@ The `SCons` constructor has an **auto-implicit** argument `{auto prf : isSorted
 - 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
+```{note}
+The `{auto prf : isSorted ...}` constraint ensures only sorted lists are generated. The `auto` keyword makes Idris search for proof automatically
 during generation.
+```
 
 ---
 
@@ -133,12 +134,13 @@ When `deriveGen` encounters `{auto prf : So $ isSorted (x :: toList xs)}`, it:
 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
+```{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.