doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
author haftmann
Wed, 22 Nov 2006 10:20:09 +0100
changeset 21452 f825e0b4d566
parent 21190 08ec81dfc7fb
child 21993 4b802a9e0738
permissions -rw-r--r--
final draft
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21190
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     1
structure ROOT = 
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     2
struct
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     3
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     4
structure Nat = 
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     5
struct
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     6
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     7
datatype nat = Zero_nat | Suc of nat;
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     8
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
     9
end; (*struct Nat*)
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    10
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    11
structure Codegen = 
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    12
struct
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    13
21452
f825e0b4d566 final draft
haftmann
parents: 21190
diff changeset
    14
val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
21190
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    15
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    16
val foobar_set : Nat.nat list =
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    17
  Nat.Zero_nat ::
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    18
    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    19
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    20
end; (*struct Codegen*)
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    21
08ec81dfc7fb (continued)
haftmann
parents:
diff changeset
    22
end; (*struct ROOT*)