Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] well founded induction computation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] well founded induction computation


chronological Thread 
  • From: Thery Laurent <thery AT ns.di.univaq.it>
  • To: rouxcody AT loria.fr
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] well founded induction computation
  • Date: Thu, 13 Nov 2008 12:54:30 +0100 (CET)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>


What is happening here? Otherwise I completely agree that programming by proof as I have done is quite disadvisable.


The problem is your two subst in your wf_fix.
Unfortunately, rewriting in dependent types makes you lose
reduction.

--
Laurent Théry

Archive powered by MhonArc 2.6.16.

Top of Page