簡単な例をコンパイル可能な Java ファイルにする

[cedretaber]

簡単な例:

From Corelib Require Extraction.
Extraction Language Java.

Inductive term :=
| Var : nat -> term
| Op : term -> term -> term.


Fixpoint size t : nat :=
	match t with 
	| Var _ => 1 
	| Op t1 t2 => 
		let s1 := size t1 in
		let s2 := size t2 in
		s1 + s2
	end.


Recursive Extraction size.