我是 Coq 的新手。我无法使用单位、产品和总和来定义列表、地图和树。我在标题中收到错误消息。评论上面的代码工作正常,下面的代码没有。
Inductive one : Type := nil : one.
Inductive sum (t0 t1 : Type) : Type :=
| inject_left : t0 -> sum t0 t1
| inject_right : t1 -> sum t0 t1.
Inductive product (t0 t1 : Type) : Type := pair : t0 -> t1 -> product t0 t1.
Definition list (t0 : Type) : Type := sum one (product t0 (list t0)).
Definition map (t0 t1 : Type) : Type := list (product t0 t1).
(* From here on nothing works. *)
Definition List (t0 : Type) : Type := sum one (product t0 (List t0)).
Definition map (t0 t1 : Type) : Type :=
sum one (product (product t0 t1) (map t0 t1)).
Definition Map (t0 t1 : Type) : Type :=
sum one (product (product t0 t1) (Map t0 t1)).
Definition tree (t0 : Type) : Type :=
sum one (product t0 (product (tree t0) (tree t0))).
Definition Tree (t0 : Type) : Type :=
sum one (product t0 (product (Tree t0) (Tree t0))).