doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
author haftmann
Thu Jan 04 17:17:48 2007 +0100 (2007-01-04)
changeset 21994 dfa5133dbe73
parent 21993 4b802a9e0738
child 22015 12b94d7f7e1f
permissions -rw-r--r--
updated manual
haftmann@21147
     1
module Codegen where
haftmann@21189
     2
import qualified Nat
haftmann@21147
     3
haftmann@21147
     4
class Null a where
haftmann@21993
     5
  nulla :: a
haftmann@21147
     6
haftmann@21993
     7
heada :: (Codegen.Null a) => ([a] -> a)
haftmann@21993
     8
heada (y : xs) = y
haftmann@21994
     9
heada [] = Codegen.nulla
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@21189
    17
dummy :: Maybe Nat.Nat
haftmann@21993
    18
dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]