当我运行以下脚本时：
Definition inv (a: Prop): Prop :=
match a with
| False => True
| True => False
end.
我收到“错误：该子句是多余的”。知道为什么会发生这种情况吗？
谢谢，
马库斯。
这件事上有不少错误的地方。
False不是数据构造函数，并且由于 Coq 中的数据构造函数和变量名称之间没有语法差异，因此它可以理解您的| False =>作为匹配任何内容的模式并为其命名False，就像你可以写的那样：
Definition inv (a: Prop): Prop :=
match a with
| x => True
| y => False
end.
这就是为什么它告诉您第二个子句是多余的（因为第一个模式匹配所有内容）。
现在你应该知道的另一件事是类型Prop不是归纳定义的，因此类型的值Prop不能与任何东西匹配：事实上它没有意义，因为它是一种开放类型，每次定义新的归纳属性时都会不断扩展。
所以没办法写函数inv你写的方式。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
