[Agda] Termination proof in partiality monad

Edsko de Vries devriese at cs.tcd.ie
Mon Nov 17 17:59:30 CET 2008


Thanks Luke/Vladimir for your answers. I did try to weaken termination  
to a terminated_with relation, but I still get stuck. Vladimir, why do  
you think it might help? Luke, would you be able to show how far you  
got? I can't even massage the lemma into such a form that fac (S n) is  
expressed in terms of fac n..

Edsko


More information about the Agda mailing list