[Agda] printing infinite structures

Guillaume Allais guillaume.allais at ens-lyon.org
Tue Feb 26 17:34:24 CET 2019


IO is coinductive so you could write `Stream String -> IO ()` in Agda itself.

On 26/02/2019 17:08, Thorsten Altenkirch wrote:
> I told them that I have no idea how to run the compiler. Which is true.
> T.
> 
> From: "Setzer A.G." <a.g.setzer at swansea.ac.uk>
> Date: Tuesday, 26 February 2019 at 15:59
> To: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>, agda list <agda at lists.chalmers.se>
> Subject: Re: printing infinite structures
> 
> The only disadvantage is that you need to compile your code, but I when interacting with students the first thing they want to know is how to compile the code.
> 
> 
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190226/139ab7bb/attachment.sig>


More information about the Agda mailing list