问题标签 [lean]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
formal-verification - 为什么精益会在 eq 的引理中添加隐式变量？
以下代码有一个奇怪的行为
在向我展示 eq.symm 的类型时，我希望 check 不会考虑不相关的隐式变量 toto。这真的是故意的吗？
proof - 精益证明助手中交换环的幂等性
嗨，我正在尝试在精益证明助手中做一些数学运算，看看它是如何工作的。我认为与交换环的幂等一起玩应该很有趣。这是我尝试过的：
然后我得到错误
所以 Lean 似乎忘记了 A 是一个环？
例如，如果我将定义更改为
那么一切都很好。但这意味着我必须携带额外的簿记数据。有没有办法使用变量来解决保留簿记的需要。
decidable - 精益抱怨它看不到一个声明是可判定的
我正在尝试定义以下数量部分：
但得到错误
由于 Hdecp，我如何帮助 Lean 认识到 (pi p) 确实是可判定的？
formal-methods - 不能使类型类在精益中工作
我无法理解如何触发 Lean 对类型类的使用。这是一个小例子的尝试：
关键是我希望 Lean 看到它可以使用 HA 从引理 T 中推断出 toto A。我错过了什么？
lean - 在精益定理证明器中使用策略模式获取
如何使用形状假设
在战术模式？在术语模式下，我会使用
proof - 什么构成了精益的有效类型？
我已经完成了精益教程的前 3 章，并且已经完成了一些命题逻辑的证明。
现在我试着回过头来问自己一些愚蠢的问题。
我的理解是：
- 术语可以有类型：
constant A : Type.A是一个术语，Type是 的类型A。 - 术语可以变成类型：
constant a : A. - 一个术语的类型可以取决于另一个术语的类型
constant B : A -> Type：constant B' : Π (a : A), Type
但是这种理解显然是错误的，因为这段代码没有进行类型检查：
开头的所有行constant C，即第 9、11 和 13 行都会抛出错误error: type expected at B
为什么？我怀疑并非所有术语都可以成为类型。我怀疑类型依赖于其他类型的术语不能成为 types。为什么？
dependent-type - 如何在精益中定义互归纳命题？
我尝试使用归纳数据类型的语法，但它收到一条错误消息“相互归纳类型必须编译为具有依赖消除的基本归纳类型”。
下面是我尝试定义命题even和odd自然数的示例
还有一个相关的问题：定义相互递归函数的语法是什么？我似乎无法在任何地方找到它的记录。
recursion - 为什么精益强制递归类型参数出现在非递归参数之后？
精益拒绝以下定义：
带有错误消息“'natlist.cons' 的 arg #2 不是递归的，但它发生在递归参数之后”
正如预期的那样，接受以下定义：
精益执行此命令的原因是什么？