doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
author haftmann
Mon Nov 06 16:28:29 2006 +0100 (2006-11-06)
changeset 21189 5435ccdb4ea1
parent 21147 737a94f047e3
child 21993 4b802a9e0738
permissions -rw-r--r--
(continued)
     1 module Codegen where
     2 import qualified Nat
     3 
     4 class Null a where
     5   null :: a
     6 
     7 head :: (Codegen.Null a_1) => [a_1] -> a_1
     8 head (y : xs) = y
     9 head [] = Codegen.null
    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.head [Just (Nat.Suc Nat.Zero_nat), Nothing]