atrieu

Fixpoint sum (l : list nat) : nat :=
  match l with
  | nil => 0
  | cons x xs => x + sum xs
  end.

Fixpoint sum_tail' (l : list nat) (acc : nat) : nat :=
  match l with
  | nil => acc
  | cons x xs => sum_tail' xs (x + acc)

atrieu

Require Import Omega.

Fixpoint fib (n : nat) :=
  match n with
  | 0 => 1
  | S n' => match n' with
            | 0 => 1
            | S n'' => fib n' + fib n''
            end
  end.