Library Coqdoc.details

Definition foo : nat := 3.

Fixpoint idnat (x : nat) : nat :=
  match x with
  | S x ⇒ S (idnat x)
  | 0 ⇒ 0
  end.