时间戳

首页 > 解决方案 > 从不同类型转换

coq - 从不同类型转换

问题描述

 Inductive color: Type :=
 | red 
 | green
 | blue.
Inductive listw : Type :=
  | nil : listw
  | cons : web -> listw -> listw.
Definition colorlist (c:color) : listw :=
  match w with 
  | red => (cons red nil)
  | green => (cons green nil)
  | blue => (cons blue nil)
end.
Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).
Definition bag:=listw.
Definition bag:=((cons red nil)++(cons green nil)++(cons blue nil)).
Bag = cons red (cons green (cons blue nil)).

我已经定义了颜色列表（感应类型）。想用特定的自然数替换每种颜色。我在将自然数分配给不同的归纳类型列表时遇到问题。

标签： coq

解决方案

我很难弄清楚你到底想要什么，所以我会试着为我所知道的写一个答案。

你有一种颜色：

Inductive color := 
| red
| green
| blue.

然后你想从中得到一个自然数列表。因此，您将数字与每种颜色相关联：

Definition nat_of_color (c : color) : nat :=
  match c with
  | red => 0
  | green => 1
  | blue => 2
  end.

现在，如果你使用listcoq 提供的类型，你想要的函数是：

Definition nat_list_of_color_list (l : list color) : list nat :=
  List.map nat_of_color l.

换句话说，List.map nat_of_color是您似乎想要的功能。

请注意，排序算法和出现计数可能会变得更通用，以便立即使用颜色。

推荐阅读