| ▲ | black_knight 41 minutes 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_. | ||