doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
author haftmann
Thu Apr 26 13:32:55 2007 +0200 (2007-04-26)
changeset 22798 e3962371f568
parent 22751 1bfd75c1f232
child 24421 acfb2413faa3
permissions -rw-r--r--
updated doc
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@22188
    13
null_option :: Maybe a;
haftmann@22015
    14
null_option = Nothing;
haftmann@21147
    15
haftmann@22015
    16
instance Codegen.Null (Maybe b) where {
haftmann@22015
    17
  nulla = Codegen.null_option;
haftmann@22015
    18
};
haftmann@21147
    19
haftmann@22015
    20
dummy :: Maybe Nat.Nat;
haftmann@22015
    21
dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing];
haftmann@21147
    22
haftmann@22015
    23
}