plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.37k stars 315 forks source link

Add an explanation of mutually recursive functions somewhere #879

Closed michaelpj closed 1 year ago

michaelpj commented 1 year ago

Probably near where the odd/even example is given, since the exercises for that section require mutually recursive functions (or at least my solutions did).

michaelpj commented 1 year ago

i.e. in Relations.

wadler commented 1 year ago

Thanks!

I was wrong, there is already an example in Quantifiers, exactly where you said it should be, with the mutually recursive functions for proving the example with Even and Odd.

Go well, -- P


From: Michael Peyton Jones @.> Sent: 31 May 2023 09:05 To: plfa/plfa.github.io @.> Cc: Subscribed @.***> Subject: [plfa/plfa.github.io] Add an explanation of mutually recursive functions somewhere (Issue #879)

This email was sent to you by someone outside the University. You should only click on links or attachments if you are certain that the email is genuine and the content is safe.

Probably near where the odd/even example is given, since the exercises for that section require mutually recursive functions (or at least my solutions did).

— Reply to this email directly, view it on GitHubhttps://github.com/plfa/plfa.github.io/issues/879, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ABFJ7MRT77RTKZXD7FQSMTTXI33TLANCNFSM6AAAAAAYVCGBBY. You are receiving this because you are subscribed to this thread.Message ID: @.***>

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhun Eideann, claraichte an Alba, aireamh claraidh SC005336.

wadler commented 1 year ago

I mean, it is in Relations, exactly where Michael said it should be.

wadler commented 1 year ago

Everything is copacetic. Thanks to Michael for his help.