doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
author wenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056 743f3603ba8b
parent 24628 33137422d7fd
child 25182 64e3f45dc6f4
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
wenzelm@25056
    13
null_option :: Maybe a;
wenzelm@25056
    14
null_option = Nothing;
wenzelm@25056
    15
haftmann@24628
    16
instance Codegen.Null (Maybe a) where {
wenzelm@25056
    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
}