问精益4无效字段表示法
EN

Stack Overflow用户

提问于 2021-09-09 13:50:56

回答 1查看 62关注 0票数 0

最小不起作用的示例：

#check Or.intro_left

给出

error: invalid field notation, type is not of the form (C ...) where C is a constant
  Or
has type
  Prop → Prop → Prop

在我的机器上。

一些实验似乎表明，每当使用.访问元素(不确定这是否是正确的术语)时，就会出现错误。

发布于 2021-09-09 14:00:18

#check Or.inl起作用了。我认为这只是因为在Lean4中没有名为Or.intro_left的声明。

票数 1

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

原文链接：

https://stackoverflow.com/questions/69119450

复制

相似问题

问精益4无效字段表示法EN