isabelle: doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs@4b802a9e0738 (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
21147 737a94f047e3 continued tutorial haftmann parents: diff changeset	9
737a94f047e3 continued tutorial haftmann parents: diff changeset	10	null_option :: Maybe b
737a94f047e3 continued tutorial haftmann parents: diff changeset	11	null_option = Nothing
737a94f047e3 continued tutorial haftmann parents: diff changeset	12
737a94f047e3 continued tutorial haftmann parents: diff changeset	13	instance Codegen.Null (Maybe b) where
737a94f047e3 continued tutorial haftmann parents: diff changeset	14	null = Codegen.null_option
737a94f047e3 continued tutorial haftmann parents: diff changeset	15
21189 5435ccdb4ea1 (continued) haftmann parents: 21147 diff changeset	16	dummy :: Maybe Nat.Nat
21993 4b802a9e0738 updated manual haftmann parents: 21189 diff changeset	17	dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]

author	haftmann
	Thu, 04 Jan 2007 17:11:09 +0100
changeset 21993	4b802a9e0738
parent 21189	5435ccdb4ea1
child 21994	dfa5133dbe73
permissions	-rw-r--r--