Skip to content

Commit

Permalink
Docs: tweak features.md
Browse files Browse the repository at this point in the history
  • Loading branch information
anuyts authored and omelkonian committed Oct 3, 2024
1 parent 0412c42 commit afb5392
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion docs/source/features.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit afb5392

Please sign in to comment.