| author | haftmann |
| Tue, 03 Mar 2009 11:00:51 +0100 | |
| changeset 30209 | 2f4684e2ea95 |
| parent 25731 | doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs@b3e415b0cf5c |
| permissions | -rw-r--r-- |
| haftmann@22015 | 1 |
module Codegen where {
|
| haftmann@21147 | 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@21147 | 8 |
|
| wenzelm@25731 | 9 |
heada :: forall a. (Codegen.Null a) => [a] -> a; |
| haftmann@22751 | 10 |
heada (x : xs) = x; |
| haftmann@22015 | 11 |
heada [] = Codegen.nulla; |
| haftmann@21147 | 12 |
|
| wenzelm@25731 | 13 |
null_option :: forall a. 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@22015 | 19 |
|
| haftmann@22015 | 20 |
dummy :: Maybe Nat.Nat; |
| haftmann@22015 | 21 |
dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]; |
| haftmann@22015 | 22 |
|
| haftmann@22015 | 23 |
} |