Why does Idris think a prefix of an identifier is a keyword?

user_11672072 0
Viewed 97

When trying to interpret this code

injective : {A : Type} ->
            {P : A -> Type} ->
            ((x : A) -> P x) ->
            Type

I get the error

   |
14 | injective : {A : Type} ->
   |           ^
not a terminator

which really confused my. When I write private over the declaration, the error seems to go away, so I guess those access modifiers really change the way parsing works. However, I don't understand why that should be.

So why does that error show up? Why does the parser think in is a keyword (which I'm guessing is the problem) instead of part of an identifier, if I don't place private just before?

[EDIT]: To get the error, this code should be enough:

Subset : Type -> Type
Subset a = a -> Type

syntax [x] "in" [y] = y x

Test : Type
Test = Nat

injective : {a, b : Type} ->
            (a -> b) ->
            Type
injective {a} {b} f = (x, y : a) ->
                      f x = f y ->
                            x = y

I'm using Idris 1.3.1's interpreter.

idris internals
1 Answers

Your code compiles just fine for me. When I had the not a terminator errors in the past it was almost always due to some indentation mistake I made. But I have no idea what the private modifier would change, so that it works in your case.

user_10407850
Related