doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
author haftmann
Thu Jan 04 17:11:09 2007 +0100 (2007-01-04)
changeset 21993 4b802a9e0738
parent 21189 5435ccdb4ea1
child 21994 dfa5133dbe73
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@21147
     9
haftmann@21147
    10
null_option :: Maybe b
haftmann@21147
    11
null_option = Nothing
haftmann@21147
    12
haftmann@21147
    13
instance Codegen.Null (Maybe b) where
haftmann@21147
    14
  null = Codegen.null_option
haftmann@21147
    15
haftmann@21189
    16
dummy :: Maybe Nat.Nat
haftmann@21993
    17
dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]