doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
changeset 22015 12b94d7f7e1f
parent 21994 dfa5133dbe73
child 22188 a63889770d57
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Jan 05 14:30:08 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Jan 05 14:31:44 2007 +0100
     1.3 @@ -1,18 +1,23 @@
     1.4 -module Codegen where
     1.5 -import qualified Nat
     1.6 +module Codegen where {
     1.7 +
     1.8 +import qualified Nat;
     1.9  
    1.10 -class Null a where
    1.11 -  nulla :: a
    1.12 +class Null a where {
    1.13 +  nulla :: a;
    1.14 +};
    1.15 +
    1.16 +heada :: (Codegen.Null a) => [a] -> a;
    1.17 +heada (y : xs) = y;
    1.18 +heada [] = Codegen.nulla;
    1.19  
    1.20 -heada :: (Codegen.Null a) => ([a] -> a)
    1.21 -heada (y : xs) = y
    1.22 -heada [] = Codegen.nulla
    1.23 +null_option :: Maybe b;
    1.24 +null_option = Nothing;
    1.25  
    1.26 -null_option :: Maybe b
    1.27 -null_option = Nothing
    1.28 +instance Codegen.Null (Maybe b) where {
    1.29 +  nulla = Codegen.null_option;
    1.30 +};
    1.31  
    1.32 -instance Codegen.Null (Maybe b) where
    1.33 -  null = Codegen.null_option
    1.34 +dummy :: Maybe Nat.Nat;
    1.35 +dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing];
    1.36  
    1.37 -dummy :: Maybe Nat.Nat
    1.38 -dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]
    1.39 +}