mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-14 13:56:59 +03:00
commit
6b062beae0
@ -105,6 +105,10 @@ symbols:
|
||||
|
||||
:+-*/=_.?|&><!@$%^~.
|
||||
|
||||
Some operators built from these symbols can't be user defined. These are
|
||||
``:``, ``=>``, ``->``, ``<-``, ``=``, ``?=``, ``|``, ``**``,
|
||||
``==>``, ``\\``, ``%``, ``~``, ``?``, and ``!``.
|
||||
|
||||
Functions
|
||||
=========
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user