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
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:
(1 a : b)
, which says there are exactly one of these available at runtime. You could also leave off the multiplicity, as (a : b)
, which means any number are available at runtime, ortest
as erased, like
0 test : (0 a : b) -> b
then you can return x
because you're stating the result of test
is also erased.