以下代码在 Idris2 中可以正常编译：
C : Nat
C = 2
claim : C = 2
claim = Refl
C但如果不大写则失败：
c : Nat
c = 2
claim : c = 2
claim = Refl
错误信息是
警告：我们将隐式绑定以下小写名称。您可能无意中隐藏了关联的全局定义：c isshadowing Main.c 错误：在处理声明的右侧时。统一时：2 = 2 和：c = 2 不匹配：2 和 c。
有没有办法告诉 Idris 编译器不要隐藏类型中的小写全局名称？
我在 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