From Coq Require Extraction.
Module SSH.

Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

Fixpoint length (l:natlist) : nat :=
  match l with
  | nil => O
  | cons h t => S (length t)
  end.

End SSH.
Extraction "SSH" SSH.