[isabelle] Lazy list theory of L. Paulson



Dear Fellows
I was trying t load the Lazy list theory of L. Paulson in the 2014
Isabelle/HOL version but I found some errors occurring.
As for example in the definition of:

definition
  lmap       :: "('a=>'b) => 'a llist => 'b llist" where
    "lmap f l = llist_corec l (%z. case z of LNil => None
                                           | LCons y z => Some(f(y), z))"

I got the error saying that LNil is not a constructor. I recall that it is
previously defined as an abstract constructor from NIL.

Any ideas how to solve this issue?



Regards
--gh



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