coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] relevance of evaluating accessibility arguments

From: Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>
To: Judicael Courant <Judicael.Courant AT lri.fr>
Cc: Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>, Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] relevance of evaluating accessibility arguments
Date: Wed, 20 Nov 2002 15:39:07 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

OK, but what is the point to enforce normalisation in an inconsistent
context? One of the main uses of normalisation is to ensure
consistency.

Best,
JF

> If you add an inconsistent axiom such as
>
> Axiom wf : (x:A)(accessible x).
>
> and if you remove the head-constructor condition for the decreasing
> argument, then you can build terms that have no normal form:
> (f a (wf a)) here.

[Coq-Club] relevance of evaluating accessibility arguments, Jean-Francois Monin
- Re: [Coq-Club] relevance of evaluating accessibility arguments, Pierre Courtieu
  - Re: [Coq-Club] relevance of evaluating accessibility arguments, Randy Pollack
    - lRe: [Coq-Club] relevance of evaluating accessibility arguments, Eduardo Gimenez
      - Re: [Coq-Club] relevance of evaluating accessibility arguments, Jean-Francois Monin
        
        Message not available
        
        Re: [Coq-Club] relevance of evaluating accessibility arguments, Jean-Francois Monin
  - Re: [Coq-Club] relevance of evaluating accessibility arguments, Jean-Francois Monin
    - Re: [Coq-Club] relevance of evaluating accessibility arguments, Judicael Courant
      - Re: [Coq-Club] relevance of evaluating accessibility arguments, Jean-Francois Monin
        
        Re: [Coq-Club] relevance of evaluating accessibility arguments, Benjamin Werner
        
        Re: [Coq-Club] relevance of evaluating accessibility arguments, Randy Pollack
- Re: [Coq-Club] relevance of evaluating accessibility arguments, Nicolas Magaud
  - Re: [Coq-Club] relevance of evaluating accessibility arguments, Venanzio Capretta
    - Re: [Coq-Club] relevance of evaluating accessibility arguments, Jean-Francois Monin