# [isabelle] HOLCF case syntax

Dear all,
I just updated
https://sourceforge.net/projects/holcf-prelude/
(something similar to the Haskell Prelude based on HOLCF) to Isabelle2014.
As already reported earlier
https://sourceforge.net/projects/holcf-prelude/
I had some trouble adapting fixrecs involving case syntax.

`This time it kind of worked. Only kind of, since it seems that it makes
``a difference whether dummy variables ("_") are used in patterns of case
``branches or not (without "_" everything seems to be fine).
`

`Please find a small theory file attached that gives an example of what I
``mean.
`
Any thoughts?
cheers
chris

theory Test
imports "~~/src/HOL/HOLCF/HOLCF"
begin
fun len
where
"len xs = (case xs of [] \<Rightarrow> 0 | _ # xs \<Rightarrow> Suc (len xs))"
no_notation
List.Nil ("[]")
domain 'a list ("[_]") =
Nil ("[]") |
Cons (lazy head :: 'a) (lazy tail :: "['a]") (infixr ":" 65)
fixrec bla
where
"bla\<cdot>xs\<cdot>y = (case xs of [] \<Rightarrow> y | x : xs \<Rightarrow> y)"
fixrec scanr :: "('a \<rightarrow> 'b \<rightarrow> 'b) \<rightarrow> 'b \<rightarrow> ['a] \<rightarrow> ['b]"
where
"scanr\<cdot>f\<cdot>q0\<cdot>[] = q0:[]" |
"scanr\<cdot>f\<cdot>q0\<cdot>(x : xs) = (
let qs = scanr\<cdot>f\<cdot>q0\<cdot>xs in
(case qs of
[] \<Rightarrow> \<bottom>
| q : qs' \<Rightarrow> f\<cdot>x\<cdot>q : qs))"
end

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*