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