doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
changeset 24421 acfb2413faa3
parent 22798 e3962371f568
child 24628 33137422d7fd
equal deleted inserted replaced
24420:9fa337721689 24421:acfb2413faa3
     8 
     8 
     9 heada :: (Codegen.Null b) => [b] -> b;
     9 heada :: (Codegen.Null b) => [b] -> b;
    10 heada (x : xs) = x;
    10 heada (x : xs) = x;
    11 heada [] = Codegen.nulla;
    11 heada [] = Codegen.nulla;
    12 
    12 
    13 null_option :: Maybe a;
       
    14 null_option = Nothing;
       
    15 
       
    16 instance Codegen.Null (Maybe b) where {
    13 instance Codegen.Null (Maybe b) where {
    17   nulla = Codegen.null_option;
    14   nulla = Nothing;
    18 };
    15 };
    19 
    16 
    20 dummy :: Maybe Nat.Nat;
    17 dummy :: Maybe Nat.Nat;
    21 dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing];
    18 dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing];
    22 
    19