July 10th, 2009 by Nils Anders Danielsson
Today Thorsten and I talked about nested fixpoints of the form μX.νY.F X Y. It turns out that such fixpoints cannot be represented directly in Agda. More details are available in a post to the Agda mailing list.
Additionally here is the whiteboard from the meeting:
munu
/Thorsten
This entry was posted
on Friday, July 10th, 2009 at 8:54 pm and is filed under Lunches.
You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.