我在 Idris 源代码中到处都看到过它，但我还没有找到它的含义的解释。我得到的最接近的是发现它RigCount在语法参考中被调用。但它是什么？
test : (0 a : b) -> b
test x = x
-- ^^^ Error
当上面的例子发生时，会抛出一个错误：While processing right hand side of test. x is not accessible in this context.
将其更改为 1 会进行类型检查，但不会进一步说明其含义。
test : (1 a : b) -> b
test x = x