Coq/SSReflect/MathComp Chapter 3

chap3.v

(* 3.1 *)
Inductive 紅白玉 :=
| 赤玉
| 白玉.

(* 3.2 *)
Print list.
(*
Inductive list (A : Type) : Type :=
    nil : list A
  | cons : A -> list A -> list A

For cons: Arguments are renamed to 
A, a, l
For nil: Argument A is implicit and
         maximally inserted
For cons: Argument A is implicit and
          maximally inserted
For list: Argument scope is [type_scope]
For nil: Argument scope is [type_scope]
For cons: Argument scopes are [type_scope
            _ list_scope]
*)
Definition 玉の列 := list 紅白玉.

(* 3.3 *)
Check nil: 玉の列.
(* Check 赤玉: 玉の列. *)
Check cons 赤玉 nil.
(* nil cons 赤玉 nil →型とか以前に意味不明 *)
Check cons 白玉 (cons 赤玉 nil).

(* 3.4 *)
Fixpoint 赤数え(balls: 玉の列) : nat :=
match balls with
| cons 赤玉 xs => S (赤数え xs)
| cons 白玉 xs => 赤数え xs
| nil => 0
end.

Compute (赤数え nil).
Compute (赤数え (cons 赤玉 nil)).
Compute (赤数え (cons 白玉 nil)).
Compute (赤数え (cons 赤玉 (cons 赤玉 nil))).