doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
changeset 21147 737a94f047e3
child 21189 5435ccdb4ea1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Fri Nov 03 14:22:33 2006 +0100
     1.3 @@ -0,0 +1,18 @@
     1.4 +module Codegen where
     1.5 +import qualified IntDef
     1.6 +
     1.7 +class Null a where
     1.8 +  null :: a
     1.9 +
    1.10 +head :: (Codegen.Null a_1) => [a_1] -> a_1
    1.11 +head (y : xs) = y
    1.12 +head [] = Codegen.null
    1.13 +
    1.14 +null_option :: Maybe b
    1.15 +null_option = Nothing
    1.16 +
    1.17 +instance Codegen.Null (Maybe b) where
    1.18 +  null = Codegen.null_option
    1.19 +
    1.20 +dummy :: Maybe IntDef.Nat
    1.21 +dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing]