doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
changeset 21189 5435ccdb4ea1
parent 21147 737a94f047e3
child 21993 4b802a9e0738
equal deleted inserted replaced
21188:2aa15b663cd4 21189:5435ccdb4ea1
     1 module Codegen where
     1 module Codegen where
     2 import qualified IntDef
     2 import qualified Nat
     3 
     3 
     4 class Null a where
     4 class Null a where
     5   null :: a
     5   null :: a
     6 
     6 
     7 head :: (Codegen.Null a_1) => [a_1] -> a_1
     7 head :: (Codegen.Null a_1) => [a_1] -> a_1
    12 null_option = Nothing
    12 null_option = Nothing
    13 
    13 
    14 instance Codegen.Null (Maybe b) where
    14 instance Codegen.Null (Maybe b) where
    15   null = Codegen.null_option
    15   null = Codegen.null_option
    16 
    16 
    17 dummy :: Maybe IntDef.Nat
    17 dummy :: Maybe Nat.Nat
    18 dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing]
    18 dummy = Codegen.head [Just (Nat.Suc Nat.Zero_nat), Nothing]