by Nils Anders Danielsson on July 10, 2009.
Tagged as: Lunches.
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