coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: [Agda] Termination proof in partiality monad

From: Edsko de Vries <devriese AT cs.tcd.ie>
To: Luke Palmer <lrpalmer AT gmail.com>
Cc: coq-club <coq-club AT pauillac.inria.fr>, "Agda mailing list" <agda AT lists.chalmers.se>
Subject: [Coq-Club] Re: [Agda] Termination proof in partiality monad
Date: Mon, 17 Nov 2008 16:59:30 +0000
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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

[Coq-Club] Termination proof in partiality monad, Edsko de Vries
- [Coq-Club] Re: [Agda] Termination proof in partiality monad, Luke Palmer
  - [Coq-Club] Re: [Agda] Termination proof in partiality monad, Edsko de Vries
    - Re: [Coq-Club] Re: [Agda] Termination proof in partiality monad, Vladimir Komendantsky
      - Re: [Coq-Club] Re: [Agda] Termination proof in partiality monad, Luke Palmer
        
        Re: [Coq-Club] Re: [Agda] Termination proof in partiality monad, Vladimir Komendantsky
      - Re: [Coq-Club] Re: [Agda] Termination proof in partiality monad, Edsko de Vries
- Message not available
  - Message not available
    - Message not available
      - [Coq-Club] Agda beats Coq (was: Termination proof in partiality monad), Edsko de Vries
        
        [Coq-Club] Re: Agda beats Coq, Nils Anders Danielsson
        
        [Coq-Club] Re: [Agda] Re: Agda beats Coq, Matthieu Sozeau
        
        [Coq-Club] Re: Agda beats Coq (was: Termination proof in partiality monad), Dan Doel
        
        [Coq-Club] Re: Agda beats Coq, Nils Anders Danielsson
        
        [Coq-Club] Re: Agda beats Coq, Nils Anders Danielsson