Archived tweet #9622 from the @leastfixedpoint Twitter Archive

@DRMacIver Having used Coq for a nontrivial proof (well, it seemed pretty bloody nontrivial to me as I sat shivering, twitching, aghast at the end of it), I'm keen to explore Agda.