Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: "Vladimir Komendantsky" <komendantsky AT gmail.com>
  • To: "Luke Palmer" <lrpalmer AT gmail.com>
  • Cc: "Agda mailing list" <agda AT lists.chalmers.se>, coq-club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Re: [Agda] Termination proof in partiality monad
  • Date: Tue, 18 Nov 2008 12:34:21 +0000
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:references; b=XaxsENwKEB4ySJ722g0mcV650xqMreHYjzrYVOozelzTlGLC+HZKcyLFaEHh/O3Bbb 9CPZhYfGS6Asd+q9jAvg0ODB2ZqOcW99/WxaNt7/HOsvtCLj0pGY940xEmau1hmweRCz opL4tNu+rYMf9VWy4kDZzbUnIPw8CrkL2FR0Y=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

2008/11/18 Luke Palmer <lrpalmer AT gmail.com>
Of course this will do it, because it is false!

fac 3 = Later (Later (Later (Now 6)))


Okay. Then my earlier remark applies. Now what you can do is define an order on [Delay A] and derive an equivalence relation "==" such that, for instance, Later (Later (Later (Now 6))) == Now 6.

V


Archive powered by MhonArc 2.6.16.

Top of Page