我可以避免小写全局变量在类型中被隐藏吗？

Question

以下代码在 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 编译器不要隐藏类型中的小写全局名称？

Answer 1

我不知道是否有编译器选项之类的，但你可以限定c. 如果它在 module 中Foo，请使用

c : Nat
c = 2

claim : Foo.c = 2
claim = Refl