[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

Sanjoy Das

More information about the Agda mailing list