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

Question

下面的代码在Idris2中可以正常编译:

C : Nat
C = 2
claim : C = 2
claim = Refl

，但如果C没有大写，则失败:

c : Nat
c = 2
claim : c = 2
claim = Refl

错误信息是

警告:我们即将隐式绑定以下小写名称。您可能无意中隐藏了相关的全局定义:c正在跟踪main错误:在处理右侧索赔时。当统一:2 = 2和:C = 22与c.不匹配

有没有办法告诉Idris编译器不要在类型中隐藏小写的全局名称?

Answer 1

我不知道是否有编译器选项或类似的，但您可以限定c。如果在模块Foo中，使用

c : Nat
c = 2
claim : Foo.c = 2
claim = Refl