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.
     1 structure Nat = 
     2 struct
     3 
     4 datatype nat = Suc of nat | Zero_nat;
     5 
     6 end; (*struct Nat*)
     7 
     8 structure Codegen = 
     9 struct
    10 
    11 type 'a null = {null : 'a};
    12 fun null (A_:'a null) = #null A_;
    13 
    14 fun head A_ (x :: xs) = x
    15   | head A_ [] = null A_;
    16 
    17 val null_option : 'a option = NONE;
    18 
    19 fun null_optiona () = {null = null_option} : ('a option) null;
    20 
    21 val dummy : Nat.nat option =
    22   head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE];
    23 
    24 end; (*struct Codegen*)