doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
author haftmann
Fri Nov 03 14:22:33 2006 +0100 (2006-11-03)
changeset 21147 737a94f047e3
child 21189 5435ccdb4ea1
permissions -rw-r--r--
continued tutorial
     1 module Codegen where
     2 import qualified IntDef
     3 
     4 class Null a where
     5   null :: a
     6 
     7 head :: (Codegen.Null a_1) => [a_1] -> a_1
     8 head (y : xs) = y
     9 head [] = Codegen.null
    10 
    11 null_option :: Maybe b
    12 null_option = Nothing
    13 
    14 instance Codegen.Null (Maybe b) where
    15   null = Codegen.null_option
    16 
    17 dummy :: Maybe IntDef.Nat
    18 dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing]