问我能避免小写全局变量在类型中被隐藏吗？
EN

Stack Overflow用户

提问于 2022-07-19 21:26:49

回答 1查看 46关注 0票数 4

以下代码可以在Idris2中编译：

C : Nat
C = 2

claim : C = 2
claim = Refl

但是，如果C没有大写，它就失败了：

c : Nat
c = 2

claim : c = 2
claim = Refl

错误信息是

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

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

回答已采纳

发布于 2022-07-19 21:33:55

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

c : Nat
c = 2

claim : Foo.c = 2
claim = Refl

票数 5

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/73043657

复制

相似问题

问我能避免小写全局变量在类型中被隐藏吗？EN