[coq]using Fin module

gistfile1.txt

Require Import Fin.
Print Module Fin.

(** Finはfinite setの略で、Fin.t n でサイズnの有限の集合を表わす型。 *)

Print Fin.t.
(* Inductive t : nat -> Set := *)
(*     F1 : forall n : nat, t (S n) | FS : forall n : nat, t n -> t (S n) *)

Check F1: Fin.t 3.              (* 0 *)
Check FS F1 :Fin.t 3.           (* 1 *)
Check FS (FS F1) :Fin.t 3.      (* 2 *)

(* Check FS (FS (FS F1)) :Fin.t 3. ==> Error *)

Check @F1 2.
(* F1 *)
(*      : t 3 *)

Check @FS 2 (@F1 1).
(* FS F1 *)
(*      : t 3 *)

Check @FS 2 (@FS 1 (@F1 0)).
(* FS (FS F1) *)
(*      : t 3 *)