doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
author haftmann
Fri Aug 24 14:14:17 2007 +0200 (2007-08-24)
changeset 24421 acfb2413faa3
parent 22798 e3962371f568
child 24628 33137422d7fd
permissions -rw-r--r--
updated
haftmann@22015
     1
module Codegen where {
haftmann@22015
     2
haftmann@22015
     3
import qualified Nat;
haftmann@21147
     4
haftmann@22015
     5
class Null a where {
haftmann@22015
     6
  nulla :: a;
haftmann@22015
     7
};
haftmann@22015
     8
haftmann@22798
     9
heada :: (Codegen.Null b) => [b] -> b;
haftmann@22751
    10
heada (x : xs) = x;
haftmann@22015
    11
heada [] = Codegen.nulla;
haftmann@21147
    12
haftmann@22015
    13
instance Codegen.Null (Maybe b) where {
haftmann@24421
    14
  nulla = Nothing;
haftmann@22015
    15
};
haftmann@21147
    16
haftmann@22015
    17
dummy :: Maybe Nat.Nat;
haftmann@22015
    18
dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing];
haftmann@21147
    19
haftmann@22015
    20
}