[Agda] termination proofs

Sanjoy Das sanjoy at playingwithpointers.com
Mon Sep 24 16:05:46 CEST 2012


Hi Serge,

You can use the Acc data type in Induction.WellFounded to explicitly
prove to Agda that your recursion terminates.

At the risk of tooting my own horn, here is a post I wrote on this
topic a few weeks back: http://playingwithpointers.com/archives/867

Cheers!
-- 
Sanjoy Das
http://playingwithpointers.com


More information about the Agda mailing list