natlist

natlist.v

Inductive natlist : Type :=
  | nnil : natlist
  | ncons : nat -> natlist -> natlist.

Check natlist_ind.
(* ===> (modulo a little variable renaming for clarity)
   natlist_ind :
      forall P : natlist -> Prop,
         P nnil  ->
         (forall (n : nat) (l : natlist), P l -> P (ncons n l)) ->
         forall n : natlist, P n *)

Inductive natlist1 : Type :=
  | nnil1 : natlist1
  | nsnoc1 : natlist1 -> nat -> natlist1.

(** Now what will the induction principle look like? *)
(* Expected: forall P : natlist1 -> Prop,
     P nnill1 ->
     (forall (l : natlist1) (n : nat), P l -> P (nsnoc1 l n)) ->
     forall n : natlist1, P n
*)
Check natlist1_ind.
(* natlist1_ind *)
(*      : forall P : natlist1 -> Prop, *)
(*        P nnil1 -> *)
(*        (forall n : natlist1, P n -> forall n0 : nat, P (nsnoc1 n n0)) -> *)
(*        forall n : natlist1, P n *)