Re: [Hol-info] Extension of Co-algebraic Datatype

> Stream L = L > > > > Best wishes, > > Michael > > > > > > > > From: Waqar Ahmad <12phdwah...@seecs.edu.pk <mailto:12phdwah...@seecs.edu.pk>> > Date: Saturday, 12 May 2018 at 05:45 > To: "Norrish, Michael (Data61, Acton)&qu

Re: [Hol-info] Extension of Co-algebraic Datatype

> > > > You might as well write the equivalent > > > > Stream L = L > > > > Best wishes, > > Michael > > > > > > > > *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk> > *Date: *Saturday, 12 May 2018 at 05:45 > *To: *"Norri

Re: [Hol-info] Extension of Co-algebraic Datatype

ael (Data61, Acton)" <michael.norr...@data61.csiro.au> Cc: hol-info <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] Extension of Co-algebraic Datatype Great!. This is exactly what I want. Thanks for helping me out...:) I located the file "CoIndDefLib" in the

Re: [Hol-info] Extension of Co-algebraic Datatype

st wishes, > > Michael > > > > > > > > *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk> > *Date: *Saturday, 12 May 2018 at 05:45 > > *To: *"Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au> > *Cc: *hol-info <h

Re: [Hol-info] Extension of Co-algebraic Datatype

fo <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] Extension of Co-algebraic Datatype Thanks!. I understand that the working of LNIL and LCONS constructors since I'm exploring "llistTheory" for quite some time. To be very clear, I'm in the process of porting "st

Re: [Hol-info] Extension of Co-algebraic Datatype

> > Michael > > > > *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk> > *Date: *Monday, 7 May 2018 at 11:38 > *To: *"Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au> > *Cc: *hol-info <hol-info@lists.sourceforge.net> > *Subject

Re: [Hol-info] Extension of Co-algebraic Datatype

Thanks for the explanation. Let me state it clearly. Can I write down a constructor of type (α -> bool) -> α​​ llist On Sun, May 6, 2018 at 8:39 PM, wrote: > I think you may be able to make your needs more precise by explicitly > considering what your

Re: [Hol-info] Extension of Co-algebraic Datatype

I think you may be able to make your needs more precise by explicitly considering what your co-algebra would be. In particular, write down the type of the “general” destructor myType -> F(myType) For lazy lists, this is α llist -> (α # α llist) option For the co-algebraic numbers it’s