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
     1 module Codegen where
     2 import qualified Nat
     3 
     4 class Null a where
     5   nulla :: a
     6 
     7 heada :: (Codegen.Null a) => ([a] -> a)
     8 heada (y : xs) = y
     9 heada [] = Codegen.nulla
    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 Nat.Nat
    18 dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]