idrisidris2

What does the 0 or 1 before a parameter name mean in Idris?


I've seen it here and there in Idris source code, but I have yet to find an explanation for what it means. The closest I've gotten is finding that it's called RigCount in the syntax reference. But what is it?

test : (0 a : b) -> b
test x = x
--      ^^^ Error

As it happens the above example throws an error: While processing right hand side of test. x is not accessible in this context.

Changing this to a 1 makes it type check, but it doesn't give any more indication what it means.

test : (1 a : b) -> b
test x = x

Solution

  • To elaborate on the error message, in the first example, (0 a : b) says there are 0 of a (or x) available at runtime. You'd need it to be available at runtime to return it. Hence, it "is not accessible in this context".

    You can make it available in this context in two ways: