我在Coq玩,试图创建一个排序列表.我只是想要一个带有列表的函数,[1,2,3,2,4]并返回类似的东西Sorted [1,2,3,4]- 即取出坏的部分,但实际上并没有对整个列表进行排序.
我想我会先定义一个lesseq类型的函数(m n : nat) -> option (m <= n),然后我可以非常轻松地模拟匹配.也许这是一个坏主意.
我现在遇到的问题的症结在于(片段,底部的整个功能)
Fixpoint lesseq (m n : nat) : option (m <= n) :=
match m with
| 0 => match n with
| 0 => Some (le_n 0)
...
不是类型的; 它说它期待一个option (m <= n),但它Some (le_n 0)有类型option (0 <= 0).我不明白,因为很明显,两者m并n在这方面零,但我不知道如何告诉勒柯克说.
整个功能是:
Fixpoint lesseq (m n : nat) : option (m <= …