author | haftmann |
Tue, 03 Mar 2009 11:00:51 +0100 | |
changeset 30226 | 2f4684e2ea95 |
parent 25731 | doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs@b3e415b0cf5c |
permissions | -rw-r--r-- |
module Codegen where { import qualified Nat; class Null a where { nulla :: a; }; heada :: forall a. (Codegen.Null a) => [a] -> a; heada (x : xs) = x; heada [] = Codegen.nulla; null_option :: forall a. Maybe a; null_option = Nothing; instance Codegen.Null (Maybe a) where { nulla = Codegen.null_option; }; dummy :: Maybe Nat.Nat; dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]; }