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