> 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
>
>
>
> 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
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
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
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
>
> 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
n a HOL type.
>
>
>
> Finally, I’m afraid that there is no general tool for defining
> co-algebraic types in HOL4 at the moment.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
> *Reply-To: *Waqar Ahmad <
ol-info <hol-info@lists.sourceforge.net>
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Sunday, 6 May 2018 at 11:58
To: hol-info <hol-info@lists.sourceforge.net>
Cc: Waqar Ahmad <waqar.ah...@seecs.edu.pk>
Subject: [Hol-info] Extension of Co-algebraic Datatype
Hi,
Hi,
Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which
is developed based on the co-algebraic datatype. I understand that the
datatype *'a llist *is derived as a subset of the option type *:num -> 'a
option. * Now, I want to define a new datatype based on datatype 'a
