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
haftmann@21147
     1
module Codegen where
haftmann@21147
     2
import qualified IntDef
haftmann@21147
     3
haftmann@21147
     4
class Null a where
haftmann@21147
     5
  null :: a
haftmann@21147
     6
haftmann@21147
     7
head :: (Codegen.Null a_1) => [a_1] -> a_1
haftmann@21147
     8
head (y : xs) = y
haftmann@21147
     9
head [] = Codegen.null
haftmann@21147
    10
haftmann@21147
    11
null_option :: Maybe b
haftmann@21147
    12
null_option = Nothing
haftmann@21147
    13
haftmann@21147
    14
instance Codegen.Null (Maybe b) where
haftmann@21147
    15
  null = Codegen.null_option
haftmann@21147
    16
haftmann@21147
    17
dummy :: Maybe IntDef.Nat
haftmann@21147
    18
dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing]