Inductive vector A : nat → Type :=
| nil : vector A 0
| cons : ∀ (h:A) (n:nat), vector A n → vector A (S n).

Inductive even : nat → Prop :=
| even_O : even 0
| even_S (n : nat) : odd n → even (S n)
with odd : nat → Prop :=
| odd_S (n : nat) : even n → odd (S n).

Inductive tree (A : Type) : Type :=
| leaf : tree A
| node (children : nat → tree A) : tree A.

Inductive rose (A : Type) : Type :=
| rleaf : rose A
| rnode (children : list (rose A)) : rose A.

Fixpoint is_even (n : nat) : bool :=
  match n with
  | 0 ⇒ true
  | 1 ⇒ false
  | S (S n') ⇒ is_even n'
  end.

Check fix is_even (n : nat) : bool :=
match n return bool with
| O ⇒ true
| S n0 ⇒ match n0 return bool with
  | O ⇒ false
  | S n' ⇒ is_even n'
  end
end.

Fixpoint even_is_even (n : nat) : (is_even n = true) → even n :=
  match n as x return is_even x = true → even x with
  | 0 ⇒ fun _ ⇒ even_O
  | 1 ⇒ fun (e : false = true) ⇒
    (match e in _ = x return (if x then even 1 else True) with
    | eq_refl ⇒ I end)
  | S (S n') ⇒ fun e ⇒ even_S _ (odd_S _ (even_is_even n' e))
  end.

Set Primitive Projections.
Record sig (A : Type) (B : A → Type) : Type :=
 { fst : A ; snd : B fst }. Definition pair : sig nat (fun _ ⇒ bool) :=
  {| fst := 0 ; snd := true |}. Arguments fst {A B}.
Arguments snd {A B}.
Definition fst_fun {A : Type} {B : A → Type} (p : sig A B) : A := p.(fst).

Module PosCoind.
CoInductive stream (A : Type) : Type :=
| scons (head : A) (tail : stream A) : stream A.

CoFixpoint repeat (A : Type) (a : A) : stream A := scons _ a (repeat A a).
End PosCoind.

CoInductive stream (A : Type) : Type := { head : A ; tail : stream A } .

CoFixpoint repeat (A : Type) (a : A) : stream A :=
  {| head := a ; tail := repeat A a |}.

Definition ex_falso (f : False) : nat := match f with end.
Fail Definition forbidden (o : True ∨ True) : nat :=
  match o with
  | or_introl _ ⇒ 0
  | or_intror _ ⇒ 1
  end.

Definition id (A : Type) (a : A) := a.
Fail Check (id _ id).

#[universes(polymorphic)] Definition pid@{i} (A : Type@{i}) (a : A) : A := a.
Check (pid _ pid).

Definition test : 0 = 0 := let x := 0 in (eq_refl x : 0 = 0).
Fail Definition test' : 0 = 0 := (fun x ⇒ eq_refl x : 0 = 0) 0.

Check (fun f : nat → nat ⇒ eq_refl) : ∀ f : nat → nat, f = (fun x ⇒ f x).

Check (fun p : sig nat (fun _ ⇒ bool) ⇒ eq_refl) :
  ∀ p : sig nat (fun _ ⇒ bool), p = {| fst := p.(fst) ; snd := p.(snd) |}.