doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
author haftmann
Fri Jan 05 14:31:44 2007 +0100 (2007-01-05)
changeset 22015 12b94d7f7e1f
parent 21994 dfa5133dbe73
child 22188 a63889770d57
permissions -rw-r--r--
adaptions
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@22015
     9
heada :: (Codegen.Null a) => [a] -> a;
haftmann@22015
    10
heada (y : xs) = y;
haftmann@22015
    11
heada [] = Codegen.nulla;
haftmann@21147
    12
haftmann@22015
    13
null_option :: Maybe b;
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
}