# HG changeset patch # User blanchet # Date 1379371681 -7200 # Node ID b51ebeda414d00a3c7b3f085252dc8be33b0023a # Parent d4a4b32038eb0aaf99b152670c055225671c7981 more (co)data docs diff -r d4a4b32038eb -r b51ebeda414d src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Sep 17 00:39:51 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Sep 17 00:48:01 2013 +0200 @@ -1602,7 +1602,7 @@ \item The \emph{constructor view} specifies $f$ by equations of the form \[@{text "f x\<^sub>1 \ x\<^sub>n = \"}\] -Haskell and other lazy functional programming languages support this style. +Lazy functional programming languages such as Haskell support this style. \item The \emph{destructor view} specifies $f$ by implications of the form \[@{text "\ \ is_C\<^sub>j (f x\<^sub>1 \ x\<^sub>n)"}\] and @@ -1623,6 +1623,8 @@ primcorec_notyet literate :: "('a \ 'a) \ 'a \ 'a llist" where "literate f x = LCons x (literate f (f x))" +text {* \blankline *} + primcorec_notyet siterate :: "('a \ 'a) \ 'a \ 'a stream" where "siterate f x = SCons x (siterate f (f x))" @@ -1650,6 +1652,8 @@ "ltl (literate f x) = literate f (f x)" . +text {* \blankline *} + primcorec siterate :: "('a \ 'a) \ 'a \ 'a stream" where "shd (siterate _ x) = x" | "stl (siterate f x) = siterate f (f x)" @@ -1851,6 +1855,8 @@ primcorec_notyet iterate\<^sub>i\<^sub>i :: "('a \ 'a llist) \ 'a \ 'a tree\<^sub>i\<^sub>i" where "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))" +text {* \blankline *} + primcorec_notyet iterate\<^sub>i\<^sub>s :: "('a \ 'a fset) \ 'a \ 'a tree\<^sub>i\<^sub>s" where "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))"