Idris-dev
Idris-dev copied to clipboard
Broken sections of custom operators starting with pipe '|', "expecting function name"
Custom operators starting with the | symbol seem to have a parsing/scoping issue.
Spotted here: https://github.com/LorenzoPerticone/idris-NN/issues/1
Steps to Reproduce
module Foo
infixl 0 |??
(|??) : Num a => a -> a -> a
x |?? y = x * y
issue : Int -> Int -> Int
issue x = (|?? x)
Observed Behavior
$ idris --check Foo.idr
Foo.idr:8:16:
|
8 | issue x = (|?? x)
| ^
unexpected 'x'
expecting function name
The error doesn't happen if:
- something else is used instead of the pipe symbol;
- the section is left i.e.
(x |??), this works.
idris --version: 1.3.3-git:PRE