doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML	Fri Nov 03 14:22:33 2006 +0100
@@ -0,0 +1,25 @@
+structure ROOT = 
+struct
+
+structure IntDef = 
+struct
+
+datatype nat = Zero_nat | Succ_nat of nat;
+
+fun plus_nat (Succ_nat m) n = plus_nat m (Succ_nat n)
+  | plus_nat Zero_nat y = y;
+
+fun times_nat (Succ_nat m) n = plus_nat n (times_nat m n)
+  | times_nat Zero_nat na = Zero_nat;
+
+end; (*struct IntDef*)
+
+structure Codegen = 
+struct
+
+fun fac (IntDef.Succ_nat n) = IntDef.times_nat (IntDef.Succ_nat n) (fac n)
+  | fac IntDef.Zero_nat = IntDef.Succ_nat IntDef.Zero_nat;
+
+end; (*struct Codegen*)
+
+end; (*struct ROOT*)