|
|
|
|
|
|
by black_knight
6 days ago
|
|
|
Agda has the most wonderful (terrifying?) operator syntax I know of. Any Unicode (except for a few reserved words) can be used, and you can indicate where operandi go with an underscore. For instance defining a function named _•_ would allow you to use a • b. But there is no limit to where the underscores go: the name _? Would give you x ? postfix. To define if-statements one defines the name if_then_else_. |
|
|