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
     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 
    10 null_option :: Maybe b
    11 null_option = Nothing
    12 
    13 instance Codegen.Null (Maybe b) where
    14   null = Codegen.null_option
    15 
    16 dummy :: Maybe Nat.Nat
    17 dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]