diff --git a/docs/source/features.md b/docs/source/features.md index d7675dd3..4b540cc1 100644 --- a/docs/source/features.md +++ b/docs/source/features.md @@ -299,7 +299,7 @@ five = (id :: Natural -> Natural) 5 (0-Quantity)= ## 0-Quantity Parameters -Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default quantity is `ω` if no quantity is explicitly annotated). Such parameters are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them. +Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default quantity is `ω` if no quantity is explicitly annotated). Parameters annotated with `0` are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them. Agda: ```agda