[isabelle] Lazy list theory of L. Paulson
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:
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and