doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
changeset 22386 4ebe883b02ff
parent 22015 12b94d7f7e1f
child 22798 e3962371f568
equal deleted inserted replaced
22385:cc2be3315e72 22386:4ebe883b02ff
     6 
     6 
     7 datatype nat = Zero_nat | Suc of nat;
     7 datatype nat = Zero_nat | Suc of nat;
     8 
     8 
     9 end; (*struct Nat*)
     9 end; (*struct Nat*)
    10 
    10 
       
    11 structure Integer = 
       
    12 struct
       
    13 
       
    14 fun nat_aux n i =
       
    15   (if IntInf.<= (i, (0 : IntInf.int)) then n
       
    16     else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int))));
       
    17 
       
    18 fun nat i = nat_aux Nat.Zero_nat i;
       
    19 
       
    20 end; (*struct Integer*)
       
    21 
    11 structure Codegen = 
    22 structure Codegen = 
    12 struct
    23 struct
    13 
    24 
    14 val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
    25 val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
    15 
    26 
    16 val foobar_set : Nat.nat list =
    27 val foobar_set : Nat.nat list =
    17   Nat.Zero_nat ::
    28   Nat.Zero_nat ::
    18     (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
    29     (Nat.Suc Nat.Zero_nat :: (Integer.nat (2 : IntInf.int) :: []));
    19 
    30 
    20 end; (*struct Codegen*)
    31 end; (*struct Codegen*)
    21 
    32 
    22 end; (*struct ROOT*)
    33 end; (*struct ROOT*)