[Agda] lectures on Agda

[selinger at mathstat.dal.ca]

Hi Jesper,

thanks, I created a pull request, and it failed with some "whitespace
issue". Speficially, the script $HOME/.local/bin/fix-whitespace --check
apparently failed.

But I don't know what that script is checking or how to fix it. I just
followed the same syntax as the other entries in that file.

I'm hoping that someone who knows what this is about could have a look.

Thanks, -- Peter

Jesper Cockx wrote:
> 
> Hi Peter,
> 
> The list is maintained as part of the Agda github at https://github.com/agda/agda/blob/master/doc/user-manual/getting-started/tutorial-list.rst. Feel free to make a PR to add a link to your course!
> 
> -- Jesper
> 
> On Thu, Oct 7, 2021 at 5:12 AM <selinger at mathstat.dal.ca<mailto:selinger at mathstat.dal.ca>> wrote:
> Hi all,
> 
> I gave a course on Agda this year, and have now made it available on
> this website:
> 
> https://www.mathstat.dal.ca/~selinger/agda-lectures/
> 
> I don't know who maintains the list of courses at
> https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html,
> but if whoever does that could add my course to that list, that would
> be great!
> 
> Thanks, -- Peter
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda