doc-src/IsarAdvanced/Codegen/Thy/examples/fac_case.ML
author haftmann
Thu Jan 04 17:17:48 2007 +0100 (2007-01-04)
changeset 21994 dfa5133dbe73
parent 21993 4b802a9e0738
child 22751 1bfd75c1f232
permissions -rw-r--r--
updated manual
     1 structure ROOT = 
     2 struct
     3 
     4 structure Nat = 
     5 struct
     6 
     7 datatype nat = Zero_nat | Suc of nat;
     8 
     9 fun plus_nat (Suc m) n = plus_nat m (Suc n)
    10   | plus_nat Zero_nat y = y;
    11 
    12 fun times_nat (Suc m) n = plus_nat n (times_nat m n)
    13   | times_nat Zero_nat n = Zero_nat;
    14 
    15 end; (*struct Nat*)
    16 
    17 structure Codegen = 
    18 struct
    19 
    20 fun fac n =
    21   (case n of Nat.Zero_nat => Nat.Suc Nat.Zero_nat
    22      | Nat.Suc m => Nat.times_nat n (fac m));
    23 
    24 end; (*struct Codegen*)
    25 
    26 end; (*struct ROOT*)