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

21147 737a94f047e3 continued tutorial haftmann parents: diff changeset	1	module Codegen where
737a94f047e3 continued tutorial haftmann parents: diff changeset	2	import qualified IntDef
737a94f047e3 continued tutorial haftmann parents: diff changeset	3
737a94f047e3 continued tutorial haftmann parents: diff changeset	4	class Null a where
737a94f047e3 continued tutorial haftmann parents: diff changeset	5	null :: a
737a94f047e3 continued tutorial haftmann parents: diff changeset	6
737a94f047e3 continued tutorial haftmann parents: diff changeset	7	head :: (Codegen.Null a_1) => [a_1] -> a_1
737a94f047e3 continued tutorial haftmann parents: diff changeset	8	head (y : xs) = y
737a94f047e3 continued tutorial haftmann parents: diff changeset	9	head [] = Codegen.null
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
737a94f047e3 continued tutorial haftmann parents: diff changeset	17	dummy :: Maybe IntDef.Nat
737a94f047e3 continued tutorial haftmann parents: diff changeset	18	dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing]

author	haftmann
	Fri, 03 Nov 2006 14:22:33 +0100
changeset 21147	737a94f047e3
child 21189	5435ccdb4ea1
permissions	-rw-r--r--