*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Lazy list theory of L. Paulson*From*: Ghassen HELALI <helali at encs.concordia.ca>*Date*: Thu, 29 Jan 2015 11:06:15 -0500*Sender*: gastongh05 at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Lazy list theory of L. Paulson***From:*Johannes Hölzl

**Re: [isabelle] Lazy list theory of L. Paulson***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Problem with function package
- Next by Date: Re: [isabelle] Lazy list theory of L. Paulson
- Previous by Thread: [isabelle] 1st CFP for IWC 2015 in Berlin
- Next by Thread: Re: [isabelle] Lazy list theory of L. Paulson
- Cl-isabelle-users January 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list