You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: docs/source/tutorials/t00-installation-and-setup.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -195,4 +195,4 @@ Green : TrafficLight
195
195
196
196
Now that you have a working setup, you are ready to learn the fundamentals of generator creation:
197
197
198
-
***Continue to Tutorial 1:**[The Generator Monad](01-generator-monad.md) to learn how to create generators manually using `pure`, `elements`, `choose`, and other combinators.
198
+
***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.
This tutorial assumes you have completed [Installation and First Steps](00-installation-and-setup.md) and have a working Idris 2 installation with DepTyCheck configured.
23
+
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.
24
24
25
25
---
26
26
@@ -225,5 +225,5 @@ Finally, let's generate a list of test users. You can use the `listOf` combinato
225
225
226
226
You've mastered the basics. Where you go next depends on your needs:
227
227
228
-
* **Want to handle types that might be empty?** Continue to [Handling Emptiness](02-handling-emptiness.md) to learn about `Gen0`, `empty`, and `pick`.
229
-
* **Ready to have `DepTyCheck` do the work for you?** Continue to [Automatic Generator Derivation](04-automatic-generator-derivation.md) to learn about `deriveGen`.
228
+
* **Want to handle types that might be empty?** Continue to [Handling Emptiness](t02-handling-emptiness.md) to learn about `Gen0`, `empty`, and `pick`.
229
+
* **Ready to have `DepTyCheck` do the work for you?** Continue to [Automatic Generator Derivation](t04-automatic-generator-derivation.md) to learn about `deriveGen`.
Copy file name to clipboardExpand all lines: docs/source/tutorials/t02-handling-emptiness.md
+3-3Lines changed: 3 additions & 3 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,6 +1,6 @@
1
1
# 2. Handling Emptiness: When a Type Has No Values
2
2
3
-
In the [first tutorial](01-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.
3
+
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.
4
4
5
5
But what happens when a type might be **uninhabited** (have no values at all) under certain conditions?
6
6
@@ -28,7 +28,7 @@ Nothing : Maybe (Fin 0)
28
28
29
29
## Prerequisites
30
30
31
-
This tutorial assumes you have completed [Installation and First Steps](00-installation-and-setup.md) and the first tutorial, ["The Generator Monad"](01-generator-monad.md).
31
+
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).
32
32
33
33
---
34
34
@@ -163,4 +163,4 @@ This demonstrates another critical aspect of `Gen0`: it allows for speculative g
163
163
164
164
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.
165
165
166
-
* **Next Tutorial:** Continue to **[Measuring Your Test Coverage](03-measuring-test-coverage.md)** to learn how to analyze the quality of your generated data.
166
+
* **Next Tutorial:** Continue to **[Measuring Your Test Coverage](t03-measuring-test-coverage.md)** to learn how to analyze the quality of your generated data.
This tutorial assumes you have completed [Installation and First Steps](00-installation-and-setup.md) and the first two tutorials on [basic generation](01-generator-monad.md) and [emptiness handling](02-handling-emptiness.md).
20
+
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).
21
21
22
22
---
23
23
@@ -163,4 +163,4 @@ Besides aggregated reports, labels are also an invaluable tool for debugging. Yo
163
163
164
164
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.
165
165
166
-
* **Next Tutorial:** Continue to **[Automatic Generator Derivation](04-automatic-generator-derivation.md)** to learn how to use `deriveGen`.
166
+
* **Next Tutorial:** Continue to **[Automatic Generator Derivation](t04-automatic-generator-derivation.md)** to learn how to use `deriveGen`.
Copy file name to clipboardExpand all lines: docs/source/tutorials/t04-automatic-generator-derivation.md
+4-4Lines changed: 4 additions & 4 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -15,7 +15,7 @@ In this tutorial, we will use a single, running example—a file system `Entry`
15
15
16
16
## Prerequisites
17
17
18
-
- Completion of [Installation and First Steps](00-installation-and-setup.md) and the tutorials on [manual generation](01-generator-monad.md), [emptiness](02-handling-emptiness.md), and [coverage analysis](03-measuring-test-coverage.md).
18
+
- 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).
19
19
20
20
---
21
21
@@ -187,6 +187,6 @@ This powerful pattern allows you to create highly flexible generators that adapt
187
187
188
188
Now that you know how to automatically generate data and provide hints, you are ready for more advanced topics:
189
189
190
-
* **Want to learn how to control what gets generated?** Continue to **[DeriveGen Signatures](05-derivegen-signatures.md)** to learn how to use given vs generated parameters and dependent pairs in signatures.
191
-
* **Want to understand how recursion affects generation?** Continue to **[Beyond Fuel](06-beyond-fuel.md)** to learn about `SpendingFuel` vs `StructurallyDecreasing` recursion.
192
-
* **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](07-derivation-tuning.md)** to learn how to use `instance` declarations to control constructor probabilities and argument generation order.
190
+
* **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.
191
+
* **Want to understand how recursion affects generation?** Continue to **[Beyond Fuel](t06-beyond-fuel.md)** to learn about `SpendingFuel` vs `StructurallyDecreasing` recursion.
192
+
* **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](t07-derivation-tuning.md)** to learn how to use `instance` declarations to control constructor probabilities and argument generation order.
Copy file name to clipboardExpand all lines: docs/source/tutorials/t05-derivegen-signatures.md
+3-3Lines changed: 3 additions & 3 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -16,7 +16,7 @@ This will give you a deep understanding of how to use signatures to control `der
16
16
17
17
## Prerequisites
18
18
19
-
- All previous tutorials, especially [Measuring Your Test Coverage](03-measuring-test-coverage.md).
19
+
- All previous tutorials, especially [Measuring Your Test Coverage](t03-measuring-test-coverage.md).
20
20
21
21
---
22
22
@@ -154,5 +154,5 @@ Let's combine the patterns we've learned. Our final generator will be the most f
154
154
155
155
Now that you know how to control `deriveGen` through signatures, you are ready for more advanced topics:
156
156
157
-
* **Want to understand how recursion affects generation?** Continue to **[Beyond Fuel: Structural Recursion](06-beyond-fuel.md)** to learn about `SpendingFuel` vs `StructurallyDecreasing` recursion.
158
-
* **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](10-generating-gadts-with-proofs.md)** to see how `deriveGen` handles types like `SortedList`.
157
+
* **Want to understand how recursion affects generation?** Continue to **[Beyond Fuel: Structural Recursion](t06-beyond-fuel.md)** to learn about `SpendingFuel` vs `StructurallyDecreasing` recursion.
158
+
* **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](t10-generating-gadts-with-proofs.md)** to see how `deriveGen` handles types like `SortedList`.
Copy file name to clipboardExpand all lines: docs/source/tutorials/t06-beyond-fuel.md
+4-4Lines changed: 4 additions & 4 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -15,7 +15,7 @@ You will learn why this happens, how to recognize the difference between **`Spen
15
15
16
16
## Prerequisites
17
17
18
-
- All previous tutorials, especially [Automatic Generator Derivation](04-automatic-generator-derivation.md).
18
+
- All previous tutorials, especially [Automatic Generator Derivation](t04-automatic-generator-derivation.md).
19
19
20
20
---
21
21
@@ -191,6 +191,6 @@ This is the core optimization: when the type system guarantees termination throu
191
191
192
192
Now that you understand how `deriveGen` handles recursion, you are ready for more advanced topics:
193
193
194
-
***Want to fix biased generators?** Continue to **[Derivation Tuning](07-derivation-tuning.md)** to learn how to use `ProbabilityTuning` and `GenOrderTuning` instances.
195
-
***Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](09-mixing-manual-and-automatic.md)** to see how `deriveGen` discovers and uses your custom generators.
196
-
***Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](10-generating-gadts-with-proofs.md)** to see how `deriveGen` handles auto-implicit proof arguments.
194
+
***Want to fix biased generators?** Continue to **[Derivation Tuning](t07-derivation-tuning.md)** to learn how to use `ProbabilityTuning` and `GenOrderTuning` instances.
195
+
***Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](t09-mixing-manual-and-automatic.md)** to see how `deriveGen` discovers and uses your custom generators.
196
+
***Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](t10-generating-gadts-with-proofs.md)** to see how `deriveGen` handles auto-implicit proof arguments.
Copy file name to clipboardExpand all lines: docs/source/tutorials/t07-derivation-tuning.md
+5-5Lines changed: 5 additions & 5 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -13,7 +13,7 @@ We will tackle two common problems that cannot be solved with external generator
13
13
14
14
## Prerequisites
15
15
16
-
- Completion of [Automatic Generator Derivation](04-automatic-generator-derivation.md).
16
+
- Completion of [Automatic Generator Derivation](t04-automatic-generator-derivation.md).
17
17
- A willingness to engage with some advanced Idris concepts!
18
18
19
19
---
@@ -145,7 +145,7 @@ data LtPair : Type where
145
145
146
146
## Next Steps
147
147
148
-
* **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.
149
-
* **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](10-generating-gadts-with-proofs.md)** to see how `deriveGen` handles GADTs with auto-implicit proof arguments.
150
-
* **Want to see a real-world example?** Continue to **[Real-World Example: Generating ASTs for a DSL](11-real-world-example.md)** to build a complete generator for a simple imperative language.
151
-
* **Want to understand the internals?** Continue to **[Under the Hood: Building a deriveGen-like Macro](08-under-the-hood-a-derivegen-like-macro.md)** to learn how the derivation engine works.
148
+
* **Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](t09-mixing-manual-and-automatic.md)** to see how `deriveGen` automatically discovers and uses your custom generators.
149
+
* **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](t10-generating-gadts-with-proofs.md)** to see how `deriveGen` handles GADTs with auto-implicit proof arguments.
150
+
* **Want to see a real-world example?** Continue to **[Real-World Example: Generating ASTs for a DSL](t11-real-world-example.md)** to build a complete generator for a simple imperative language.
151
+
* **Want to understand the internals?** Continue to **[Under the Hood: Building a deriveGen-like Macro](t08-under-the-hood-a-derivegen-like-macro.md)** to learn how the derivation engine works.
0 commit comments