将整数列表转换为自然数列表
将整数列表转换为自然数列表
提问于 2013-06-06 13:34:36
我想把list of integer转换成list of nat。下面是我在Coq中返回的函数。
Fixpoint list_int_to_nat (l : list integer) : list nat :=
match l with
| nil => nil
| x :: l' => let i := Z.to_nat x in
list_int_to_nat l'
end.您能否帮助我将列表integer的每个元素转换为nat的列表，因为在我的函数中，我没有使用第一个元素i？非常感谢你的帮助。
回答 2
Stack Overflow用户
回答已采纳
发布于 2013-06-06 15:16:22
你写了一个递归函数，它总是在尾部调用自己，而你对头部没有做任何事情，所以最终，你的函数总是返回nil。
这里需要的是使用list中的cons构造函数将i添加到返回列表的开头。
Fixpoint list_int_to_nat (l : list integer) : list nat :=
match l with
| nil => nil
| x :: l' => let i := Z.to_nat x in
i :: list_int_to_nat l'
end.(在这里我使用了:：表示法，我发现它更方便)。
这应该能起到作用。
Stack Overflow用户
发布于 2013-06-06 21:28:29
您还可以使用map
Definition list_int_to_nat l := map Z.to_nat l.页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/16954361
复制相关文章
相似问题
腾讯云开发者
