该list_rec函数具有以下类型：
list_rec
: forall (A : Type) (P : list A -> Set),
P nil ->
(forall (a : A) (l : list A), P l -> P (a :: l)%list) ->
forall l : list A, P l
在我提出的所有示例中，P它只是一个常量函数，不管输入什么，它都会忽略输入列表并返回相同的类型。例如，P可能是fun _ : list A => nat或fun _ : list A => list B。有什么用例可以使输出P依赖于输入？为什么是类型P list A -> Set而不是Set？
例如，我们可以list_rec与非恒定P函数一起使用，以实现将列表转换为向量（长度索引列表）的函数。
Require List Vector.
Import List.ListNotations Vector.VectorNotations.
Set Implicit Arguments.
Section VecExample.
Variable A : Set.
Definition P (xs : list A) : Set := Vector.t A (length xs).
Definition list_to_vector : forall xs : list A, Vector.t A (length xs) :=
list_rec P [] (fun x _ vtail => x :: vtail).
End VecExample.
您可以使用的标准定义进行比较Vector.of_list的功能，这不正是（相同t手段Vector.t使用，而不是躲在背后递归原理明确的递归在下面的代码），：
Fixpoint of_list {A} (l : list A) : t A (length l) :=
match l as l' return t A (length l') with
|Datatypes.nil => []
|(h :: tail)%list => (h :: (of_list tail))
end.
一个简单的测试：
Eval compute in list_to_vector [1;2;3].
Eval compute in Vector.of_list [1;2;3].
这两个函数调用返回相同的结果：
= [1; 2; 3]
: Vector.t nat (length [1; 2; 3])
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句