Nottingham FP Lab Blog

Some observations about μν

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:

comments powered by Disqus