ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 14:38:20 +03:00
Code Issues Projects Releases Wiki Activity

List unavailable operators

Browse Source 
Fixes #1162

There is already an error message for it
This commit is contained in:
Niklas Larsson 2015-07-24 13:17:00 +02:00
parent dda41af21d
commit fc4b908c80
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
docs/tutorial/typesfuns.rst
View File

@ -105,6 +105,10 @@ symbols:
:+-*/=_.?|&><!@$%^~.
Some operators built from these symbols can't be user defined. These are
``:``, ``=>``, ``->``, ``<-``, ``=``, ``?=``, ``|``, ``**``,
``==>``, ``\\``, ``%``, ``~``, ``?``, and ``!``.
Functions
=========