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

Merge pull request #2563 from jeremy-w/patch-2

Browse Source 
Unescape '\' in list of non–user-definable symbols
This commit is contained in:
Jan de Muijnck-Hughes 2015-08-31 08:08:20 +01:00
commit fea108a4b5
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
docs/tutorial/typesfuns.rst
View File

@ -107,7 +107,7 @@ symbols:
Some operators built from these symbols can't be user defined. These are
``:``, ``=>``, ``->``, ``<-``, ``=``, ``?=``, ``|``, ``**``,
``==>``, ``\\``, ``%``, ``~``, ``?``, and ``!``.
``==>``, ``\``, ``%``, ``~``, ``?``, and ``!``.
Functions
=========