[ docs ] Remove useless Congratulations section

Author: GulinSS

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

@@ -191,18 +191,6 @@ Green : TrafficLight
 
 ---
 
-## Congratulations!
-
-You have successfully set up Idris 2 and DepTyCheck, created your first project, and run an automatic generator.
-
-In this tutorial, you learned:
-
-*   ✅ How to install Idris 2 and DepTyCheck
-*   ✅ How to create a project with the correct dependencies
-*   ✅ How to define a data type and derive a generator
-*   ✅ How to build and run a DepTyCheck project
-*   ✅ How to use the REPL for interactive testing
-
 ## Next Steps
 
 Now that you have a working setup, you are ready to learn the fundamentals of generator creation:

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

@@ -221,21 +221,6 @@ Finally, let's generate a list of test users. You can use the `listOf` combinato
 
 ---
 
-## Congratulations!
-
-You've learned the fundamentals of creating test data generators with `DepTyCheck`.
-
-You now know how to:
-*   ✅ Create a simple, constant generator with `pure`.
-*   ✅ Generate random numbers and pick from lists with `choose` and `elements`.
-*   ✅ Combine simple recipes into complex ones using `<$>` and `<*>`.
-*   ✅ Create weighted and unweighted choices with `frequency` and `oneOf`.
-*   ✅ Create dependent values using `do` notation.
-*   ✅ Generate a collection of random data with `listOf`.
-*   ✅ Run any generator to see the result using `pick1`.
-
-This pattern of building small, simple recipes and combining them into larger ones is the core of `DepTyCheck`.
-
 ## Next Steps
 
 You've mastered the basics. Where you go next depends on your needs:

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

@@ -159,18 +159,6 @@ This demonstrates another critical aspect of `Gen0`: it allows for speculative g
 
 ---
 
-## Congratulations!
-
-You can now write safe, robust generators for complex dependent types and are prepared to handle the full range of data-generating scenarios.
-
-In this tutorial, you learned how to:
-
-*   ✅ Identify types that can be uninhabited (empty).
-*   ✅ Use `Gen0` to define a generator that might not produce a value.
-*   ✅ Use `empty` to explicitly mark a generation path as impossible.
-*   ✅ Use `pick` to safely run a `Gen0` and handle the resulting `Maybe` value.
-*   ✅ Create filtered generators with `suchThat` and understand why they must also be `Gen0`.
-
 ## 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.

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

@@ -157,16 +157,7 @@ Besides aggregated reports, labels are also an invaluable tool for debugging. Yo
     ```
     In the first run, the label `"Red"` was printed to the console the moment the corresponding generator was executed. In the second run, no labels were printed. For a deeply nested generator, this trace allows you to understand exactly which path was taken to produce a specific problematic value.
 
-## Congratulations!
-
-You can now generate, analyze, and debug your test generators using labels.
-
-In this tutorial, you learned how to:
-
-*   ✅ Use `label` to instrument different paths in your generator.
-*   ✅ **Aggregate Constructor Coverage:** Use `initCoverageInfo`, `unGenTryND`, and `registerCoverage` to produce a report on which constructors were hit.
-*   ✅ **Debug Single Runs:** Use `PrintAllLabels` with `pick1` to trace the execution of a single generator run.
-*   ✅ Understand that runners like `pick1` use a default `IgnoreLabels` implementation that can be overridden with the `@{...}` syntax.
+---
 
 ## Next Steps
 

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

@@ -183,16 +183,6 @@ This powerful pattern allows you to create highly flexible generators that adapt
 
 ---
 
-## Congratulations!
-
-You have now unlocked the core power of `DepTyCheck`. You can say goodbye to writing boilerplate generators and let the compiler do the work for you, while still providing guidance when needed.
-
-In this tutorial, you learned:
-
-*   ✅ How to replace a complex, manual recursive generator with a single `deriveGen` macro.
-*   ✅ How to provide a **custom generator** for a base type like `String` by adding a `=>` constraint to the signature.
-*   ✅ How to pass **runtime arguments** to a derived generator to make it more flexible and context-aware.
-
 ## Next Steps
 
 Now that you know how to automatically generate data and provide hints, you are ready for more advanced topics:

docs/source/tutorials/05-derivegen-signatures.md

@@ -150,18 +150,6 @@ Let's combine the patterns we've learned. Our final generator will be the most f
 
 ---
 
-## Congratulations!
-
-You have learned to 'speak' to `deriveGen` through its most powerful interface: the type signature. You are no longer just asking it to generate a type; you are giving it a precise blueprint of your intent.
-
-By crafting the signature, you can control what `deriveGen` does:
-
-*   ✅ **Given Parameters (`(n : Nat) -> ...`):** Arguments before `Fuel` are treated as fixed runtime inputs.
-*   ✅ **Generated Parameters (`... -> Gen (n ** Vect n a)`):** Using `**` in the return type tells `deriveGen` to invent a value for that parameter for you.
-*   ✅ **External Generator Hints (`(...) => ...`):** A constraint tells `deriveGen` to use a generator you provide for a specific type.
-
-Mastering these three patterns gives you the power to create flexible, reusable, and precise automatic generators for indexed types like `Vect` and `Fin`.
-
 ## Next Steps
 
 Now that you know how to control `deriveGen` through signatures, you are ready for more advanced topics:

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

@@ -187,16 +187,6 @@ This is the core optimization: when the type system guarantees termination throu
 
 ---
 
-## Congratulations!
-
-You now understand the sophisticated, two-pronged approach `deriveGen` uses to handle recursion safely and efficiently. This knowledge will help you design data types that can be generated more effectively and to reason about the performance of your generators.
-
-In this tutorial, you learned:
-
-*   ✅ **`SpendingFuel` Recursion:** The default behavior for simple recursive types like `PNat` or `List`, where each recursive step consumes one unit of fuel.
-*   ✅ **`StructurallyDecreasing` Recursion:** An advanced optimization for indexed types like `Fin` or `Vect`, where `deriveGen` proves termination from type indices and doesn't spend fuel.
-*   ✅ **Under the Hood:** How `deriveGen` translates to manual Fuel pattern matching, and why the two recursion types generate different code.
-
 ## Next Steps
 
 Now that you understand how `deriveGen` handles recursion, you are ready for more advanced topics:

docs/source/tutorials/07-derivation-tuning.md

@@ -143,19 +143,6 @@ data LtPair : Type where
 
 ---
 
-## Congratulations!
-
-You have now learned the true, advanced methods for controlling `DepTyCheck`'s derivation engine. By implementing the tuning interfaces, you can provide expert guidance to the compiler, resulting in efficient and well-distributed test data for any data type.
-
-In this tutorial, you learned how to:
-
-*   ✅ **Prove Bias:** Use coverage analysis to find and prove when a default generator is not producing a good data distribution.
-*   ✅ **Tune Probabilities:** Implement the `ProbabilityTuning` interface to fix biases by giving a constructor a new `Weight`.
-*   ✅ **Tune Generation Order:** Implement the `GenOrderTuning` interface to tell `deriveGen` which arguments to generate first, making generation for constrained dependent types more efficient.
-*   ✅ Use advanced Idris features like `instance` declarations and `Name` literals to apply these tuning rules.
-
-This completes the advanced derivation tuning tutorial! You now have the tools to control `deriveGen`'s behavior for any data type.
-
 ## Next Steps
 
 *   **Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](09-mixing-manual-and-automatic.md)** to see how `deriveGen` automatically discovers and uses your custom generators.

docs/source/tutorials/08-under-the-hood-a-derivegen-like-macro.md

@@ -100,11 +100,11 @@ Now we need to create the manager that understands the `Simple` type as a whole.
         -- Get constructor info: B first (non-recursive), then A (recursive)
         let [conB, conA] = sig.targetType.cons
         let emptyGivs = empty  -- No given constructor arguments for Simple
-        
+
         -- Get the code for the two constructor bodies using our named strategies
         b_body <- consGenExpr @{MyStrategy} sig conB emptyGivs (var "fuel")
         a_body <- consGenExpr @{MyStrategy} sig conA emptyGivs (var "fuel")
-        
+
         -- Our biased logic!
         let body = `(case fuel of
                        Dry => ~b_body -- Out of fuel, MUST choose B
@@ -125,7 +125,7 @@ We have now defined a complete, custom derivation pipeline. All that's left is t
 
 ## Step 4: Create the Top-Level Macro
 
-Users don't interact with `DeriveBodyForType` directly. They use the `deriveGen` macro. The `deriveGen` function takes an optional `@` argument providing the core derivation logic. By default, this is `MainCoreDerivator @{LeastEffort}`. 
+Users don't interact with `DeriveBodyForType` directly. They use the `deriveGen` macro. The `deriveGen` function takes an optional `@` argument providing the core derivation logic. By default, this is `MainCoreDerivator @{LeastEffort}`.
 
 We will create our own macro, `myDeriveGen`, that simply calls `deriveGen` but passes our custom `MyTypeStrategy` instead.
 
@@ -244,17 +244,6 @@ main = do
 
 ---
 
-## Congratulations!
-
-You have built a working derivation macro from scratch. You now understand the fundamental architecture of `DepTyCheck`'s derivation engine and have seen that it is not magic, but a well-structured system of extensible interfaces. This is the deepest level of `DepTyCheck` mastery.
-
-In this tutorial, you learned:
-
-*   ✅ The core interfaces of the derivation engine: `DeriveBodyForType` and `DeriveBodyRhsForCon`.
-*   ✅ How the "Type Expert" delegates work to "Constructor Experts".
-*   ✅ How to implement these interfaces to create a custom derivation strategy.
-*   ✅ How to wrap up your custom logic in a top-level macro that acts just like `deriveGen`.
-
 ## Path to Contribution
 
 Understanding these internal APIs is the first step to extending `DepTyCheck`. If you find a new, useful derivation pattern or a more advanced strategy, you now have the foundational knowledge to implement it and contribute back to the project.

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

@@ -77,9 +77,7 @@ It works! `deriveGen` automatically found and used our `genSpecialString` functi
 2.  **Explicit (`=>` syntax):** As seen in Tutorial 4, you can add a `(Fuel -> Gen MaybeEmpty String) =>` constraint to the signature.
     *   **When to use:** This is best when you want to provide a generator for a *primitive* or *built-in* type (like `String`, `Nat`, `List`), or when you want the caller to be able to supply *different* generators in different contexts.
 
-## Congratulations!
-
-You've learned how to seamlessly mix automatic and manual generation, giving you the perfect balance of convenience and control.
+---
 
 ## Next Steps