如何证明在精益生产中反向为零
如何证明在精益生产中反向为零
提问于 2020-03-14 16:13:40
我已经在列表上定义了一个反向函数，我试图证明一个平凡的性质，即一个空列表的反向是空的。它应该可以通过反身性来证明：
def reverse (t : list α) : list α :=
list.rec_on t nil (λ x l r, r ++ [x])
#reduce reverse nil --outputs nil
lemma mylemma: reverse nil = nil := refl然而，当我运行这段代码时，我得到一个错误：
don't know how to synthesize placeholder
context:
⊢ Type这是什么意思？
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-03-15 05:59:01
Lean无法从上下文中推断出右侧的空列表的类型。显式传递类型参数：
lemma mylemma: reverse (nil) = @nil α :=
by refl页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/60680912
复制相关文章
相似问题
腾讯云开发者
