doc-src/Codegen/Thy/examples/fac.ML
author haftmann
Tue, 03 Mar 2009 11:00:51 +0100
changeset 30226 2f4684e2ea95
parent 25160 doc-src/IsarAdvanced/Codegen/Thy/examples/fac.ML@72fcf0832cfe
permissions -rw-r--r--
more canonical directory structure of manuals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21190
08ec81dfc7fb (continued)
haftmann
parents: 21172
diff changeset
     1
structure Nat = 
21147
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     2
struct
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     3
24421
acfb2413faa3 updated
haftmann
parents: 23850
diff changeset
     4
datatype nat = Suc of nat | Zero_nat;
21147
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
     5
25160
72fcf0832cfe updated;
wenzelm
parents: 24421
diff changeset
     6
val one_nat : nat = Suc Zero_nat;
72fcf0832cfe updated;
wenzelm
parents: 24421
diff changeset
     7
21190
08ec81dfc7fb (continued)
haftmann
parents: 21172
diff changeset
     8
fun plus_nat (Suc m) n = plus_nat m (Suc n)
22751
1bfd75c1f232 updated
haftmann
parents: 21994
diff changeset
     9
  | plus_nat Zero_nat n = n;
21147
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    10
21994
dfa5133dbe73 updated manual
haftmann
parents: 21993
diff changeset
    11
fun times_nat (Suc m) n = plus_nat n (times_nat m n)
dfa5133dbe73 updated manual
haftmann
parents: 21993
diff changeset
    12
  | times_nat Zero_nat n = Zero_nat;
21147
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    13
21190
08ec81dfc7fb (continued)
haftmann
parents: 21172
diff changeset
    14
end; (*struct Nat*)
21147
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    15
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    16
structure Codegen = 
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    17
struct
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    18
21994
dfa5133dbe73 updated manual
haftmann
parents: 21993
diff changeset
    19
fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n)
25160
72fcf0832cfe updated;
wenzelm
parents: 24421
diff changeset
    20
  | fac Nat.Zero_nat = Nat.one_nat;
21147
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    21
737a94f047e3 continued tutorial
haftmann
parents:
diff changeset
    22
end; (*struct Codegen*)