coq - 如何正式写声明？

Question

我有自然数列表，并且想设置当 l 为零时列表头不能为零的假设。像 (0::nil) 给出错误。如何正式写？我有错误信息，当写成

 ((h::nil)=?(0::nil))=false. 

标签： coq

Answer 1

例如，您可以使用 match 语句：

match xs with
 | 0::nil => False
 | _ => True
end