From 19647b0d04e1b90130f4877d3fff16d01937ec8c Mon Sep 17 00:00:00 2001 From: ice1000 Date: Wed, 19 Jun 2024 01:50:15 -0400 Subject: [PATCH] guide: improve phrasing --- aya/guide/haskeller-tutorial.aya.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/aya/guide/haskeller-tutorial.aya.md b/aya/guide/haskeller-tutorial.aya.md index 10c9b5b..5b3988f 100644 --- a/aya/guide/haskeller-tutorial.aya.md +++ b/aya/guide/haskeller-tutorial.aya.md @@ -278,6 +278,8 @@ tighter :< Imagine how much work this is in Haskell. +## Overlapping patterns + There is one more bonus: in Aya, you may modify the definition of `<+>` to be: ``` @@ -295,10 +297,14 @@ Then having `n + 0` to directly reduce to `n` is very useful, otherwise we will need to write a conversion function that does nothing but changes the type, or use `unsafeCoerce`. -With `n + 0 = n`, we may add the following clause to `++`: +With `n + 0 = n` judgmentally, we now have more possibilities. +For instance, we can make `xs ++ nil = xs`. This involves in two steps: we first turni `++` into +a `overlap def`, then we add the following clause to `++`: ``` | xs, nil => xs ``` This makes `++` compute on more cases too. + +For more information about this feature, checkout the [tutorial for proof assistant users](prover-tutorial).