模式匹配不是专业类型
|
我在Coq中玩耍，试图创建一个排序列表。
我只是想要一个接受列表takes0ѭ并返回类似
Sorted [1,2,3,4]
(m n : nat) -> option (m <= n)
lesseq
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)
n
Fixpoint lesseq (m n : nat) : option (m <= n) :=
match m with
| 0 => match n with
| 0 => Some (le_n 0)
| S n_ => None
end
| S m_ => match n with
| 0 => None
| S _ => match lesseq m_ n with
| Some x=> le_S m n x
| None => None
end
end
end.
没有找到相关结果
已邀请:
2 个回复
缕嚏冻
Fixpoint lesseq (m n : nat) : option (m <= n) := match n with | 0 => match m with | 0 => Some (le_n 0) | S m0 => None end | S p => match lesseq m p with | Some l => Some (le_S m p l) | None => None end end.Fixpoint lesseq (m n : nat) : option (m <= n) := match n return (option (m <= n)) with | 0 => match m return (option (m <= 0)) with | 0 => Some (le_n 0) | S m0 => None end | S p => match lesseq m p with | Some l => Some (le_S m p l) | None => None end end.Definition lesseq m n : option (m <= n). refine (fix lesseq (m : nat) (n : nat) {struct n} := _). destruct n. destruct m. apply Some; apply le_n. apply None. destruct (lesseq m n). apply Some. apply le_S. assumption. apply None. Defined.味芯憨
。 还要注意，您建议的功能仅会向您提供信息。对于模式匹配，和类型{ ... } + { ... }