【函数语言程序设计】4

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

Compute (square 10).