mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 14:57:30 +03:00
commit
5339208f04
@ -363,10 +363,10 @@ alternative notion of function application, with explicit calls to
|
||||
m_add' x y = m_app (m_app (Just (+)) x) y
|
||||
|
||||
Rather than having to insert ``m_app`` everywhere there is an
|
||||
application, we can use to do the job for us. To do this, we can make
|
||||
``Maybe`` an instance of ``Applicative`` as follows, where ``<*>`` is
|
||||
defined in the same way as ``m_app`` above (this is defined in the
|
||||
Idris library):
|
||||
application, we can use idiom brackets to do the job for us.
|
||||
To do this, we can make ``Maybe`` an instance of ``Applicative``
|
||||
as follows, where ``<*>`` is defined in the same way as ``m_app``
|
||||
above (this is defined in the Idris library):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user