doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML
author blanchet
Wed Mar 04 11:05:02 2009 +0100 (2009-03-04 ago)
changeset 30241 3a1aef73b2b2
parent 25182 64e3f45dc6f4
permissions -rw-r--r--
Merge.
haftmann@21190
     1
structure Nat = 
haftmann@21147
     2
struct
haftmann@21147
     3
haftmann@24421
     4
datatype nat = Suc of nat | Zero_nat;
haftmann@21147
     5
haftmann@21190
     6
end; (*struct Nat*)
haftmann@21147
     7
haftmann@21147
     8
structure Codegen = 
haftmann@21147
     9
struct
haftmann@21147
    10
haftmann@22386
    11
type 'a null = {null : 'a};
haftmann@22386
    12
fun null (A_:'a null) = #null A_;
haftmann@21147
    13
wenzelm@25182
    14
fun head A_ (x :: xs) = x
wenzelm@25182
    15
  | head A_ [] = null A_;
haftmann@21147
    16
wenzelm@25056
    17
val null_option : 'a option = NONE;
wenzelm@25056
    18
wenzelm@25056
    19
fun null_optiona () = {null = null_option} : ('a option) null;
haftmann@21147
    20
haftmann@21190
    21
val dummy : Nat.nat option =
wenzelm@25056
    22
  head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
haftmann@21147
    23
haftmann@21147
    24
end; (*struct Codegen*)