我希望能够在 Coq 中比较两个类型为“list”的项目,并得到一个 bool 值“true”或“false”来表示它们是否等价。
现在,我正在以这种方式比较两个列表:
Eval vm_compute in (list 1 = list 2).
我得到一个形式的 Prop:
= nil
:: (2 :: 3 :: nil)
:: (2 :: nil)
:: (3 :: nil) :: nil =
nil
:: (2 :: 3 :: nil)
:: (2 :: nil)
:: (3 :: nil) :: nil
: Prop
很明显 list1 = list2,那么我如何让它只返回 true 或 false?
最佳答案
我使用 Mathematical Components Library boolean equality operators :
From mathcomp Require Import all_ssreflect.
...
Eval vm_compute in list 1 == list 2
关于coq - Coq 中列表的 bool 相等性?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/50016903/