[Agda] Absurd question
m.escardo at cs.bham.ac.uk
Fri May 24 01:26:51 CEST 2013
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).
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.
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda