【发布时间】：2018-11-28 20:45:48
【问题描述】：
这里的学生，刚开始学习 Coq。我本质上是想证明 [] = a::l 其中 (a:A) 和 (l: list A) 是 False，解决所有子目标。我找到了一个名为 nil_cons 的漂亮 Coq 库函数，但在尝试应用它时出现错误。有人有建议吗？提前致谢！
【问题讨论】：
-
您能否发布您的证明尝试，包括您遇到错误的地方？
-
@ArthurAzevedoDeAmorim 我已经用证明尝试更新了我的帖子
-
这不是添加证明尝试的正确方法，请查看 [coq] 主题的其他帖子，这些帖子几乎总是包含 Coq 尝试：它们包含文本。这对于那些可以在他们的工作环境中复制粘贴您的文本的潜在助手来说更容易使用。
标签： coq coq-tactic