[Agda] Absurd question
m.escardo at cs.bham.ac.uk
Fri May 24 00:45:59 CEST 2013
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.
More information about the Agda