Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: allowing non-structurally terminating functions ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: allowing non-structurally terminating functions ?


chronological Thread 
  • From: "Samuel Bronson" <naesten AT gmail.com>
  • To: courtieu <pierre.courtieu AT gmail.com>
  • Cc: coq-club <coq-club AT pauillac.inria.fr>
  • Subject: Re: [Coq-Club] Re: allowing non-structurally terminating functions ?
  • Date: Thu, 19 Jun 2008 16:33:25 -0400
  • 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:content-transfer-encoding:content-disposition :references; b=aE5TvU8ravGVnFFHiMuDUYY8/ItfimB72n1/bvI52Puaqb0UWYI/C2WCTrjDhXJv1d DTp1XO1zDzgmsWSXUU2dxRh/0+jvCNIdMPsMhi2WWnebyOceSYC5nPFcToqQW818+sdq MZIHPjtZFGl7l2Z0DWWsyArTSCaJMTa5Knoms=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On 6/18/08, courtieu 
<pierre.courtieu AT gmail.com>
 wrote:

> Do we want to lose this property (termination of typing even in
> presence of inconsistent environments)?

It seems to me that non-termination of typing would be a fitting
punishment for incorrectly claiming that a function was terminating
...



Archive powered by MhonArc 2.6.16.

Top of Page