mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 17:21:59 +03:00
Update docs/source/reference/operators.rst
This commit is contained in:
parent
e1f4fbba83
commit
e7a4914f11
@ -250,8 +250,8 @@ A typical example of this is the dependent linear arrow:
|
||||
(=@) x f = (1 v : x) -> f v
|
||||
|
||||
|
||||
However, we cannot use as is because the second argument is
|
||||
a lambda, and writing out any value using this operator will look a bit awkward:
|
||||
However, when trying to use it in infix position, we have to use a lambda to populate the
|
||||
second argument:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user