如何证明反向零在精益中为零

Question

我已经在列表上定义了一个反向函数，并且我试图证明一个琐碎的属性，即空列表的反向是空的。应该通过反射来证明：

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

这是什么意思？

Answer 1

精益不能从上下文推断出右侧的空列表的类型。显式传递类型参数：

lemma mylemma: reverse (nil) = @nil α :=
by refl