[Agda] Absurd question

[Martin Escardo]

At the risk of polluting this list with too many messages, I make 
explicit what I said below, in the previous message:

I have two closed terms dialogue-tree and dialogue-tree' with 
(literally) the same closed type. The definition of one term uses \(), 
and the definition of the other term uses y instead.

But a certain definition (namely dialogue-tree-correct) type-checks if 
one of its subterms is dialogue-tree', but doesn't if it is 
dialogue-tree. But surely, because everything is closed, it shouldn't 
matter which term we use (even a postulated term should do).

Best,
Martin

On 23u05/13 23:45, Martin Escardo wrote:
>
>
> On 23/05/13 23:37, Martin Escardo wrote:
>> But, still, this requires redefining the natural formulations into
>> unnatural ones. (You would have to see the file to appreciate the
>> unnaturality, reported in the comments.)
>
> Ignoring the parenthetical remark, this is odd, because once a theorem
> is proved, it is proved. It shouldn't make a difference whether its
> proof uses \() or y.
>
> But in this case, the uses of the theorem are rejected if its proof uses
> \(), and accepted if its proof uses y.
>
> Martin
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe