isabelle: doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs@dfa5133dbe73 (annotated)

21147 737a94f047e3 continued tutorial haftmann parents: diff changeset	1	module Codegen where
21189 5435ccdb4ea1 (continued) haftmann parents: 21147 diff changeset	2	import qualified Nat
21147 737a94f047e3 continued tutorial haftmann parents: diff changeset	3
737a94f047e3 continued tutorial haftmann parents: diff changeset	4	class Null a where
21993 4b802a9e0738 updated manual haftmann parents: 21189 diff changeset	5	nulla :: a
21147 737a94f047e3 continued tutorial haftmann parents: diff changeset	6
21993 4b802a9e0738 updated manual haftmann parents: 21189 diff changeset	7	heada :: (Codegen.Null a) => ([a] -> a)
4b802a9e0738 updated manual haftmann parents: 21189 diff changeset	8	heada (y : xs) = y
21994 dfa5133dbe73 updated manual haftmann parents: 21993 diff changeset	9	heada [] = Codegen.nulla
21147 737a94f047e3 continued tutorial haftmann parents: diff changeset	10
737a94f047e3 continued tutorial haftmann parents: diff changeset	11	null_option :: Maybe b
737a94f047e3 continued tutorial haftmann parents: diff changeset	12	null_option = Nothing
737a94f047e3 continued tutorial haftmann parents: diff changeset	13
737a94f047e3 continued tutorial haftmann parents: diff changeset	14	instance Codegen.Null (Maybe b) where
737a94f047e3 continued tutorial haftmann parents: diff changeset	15	null = Codegen.null_option
737a94f047e3 continued tutorial haftmann parents: diff changeset	16
21189 5435ccdb4ea1 (continued) haftmann parents: 21147 diff changeset	17	dummy :: Maybe Nat.Nat
21993 4b802a9e0738 updated manual haftmann parents: 21189 diff changeset	18	dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]

author	haftmann
	Thu, 04 Jan 2007 17:17:48 +0100
changeset 21994	dfa5133dbe73
parent 21993	4b802a9e0738
child 22015	12b94d7f7e1f
permissions	-rw-r--r--