[Agda] A philosophical question on absurd.

[David Banas]

Hi all,

I'm brand new to Agda and the Curry-Howard isomorphism (and really loving
this new exploration of both!), and I have a *philosophical* objection to
how the *absurd* function is used to generate whatever we need to complete
a proof.

I understand how we are able to satisfy the Agda compiler with the
definition of *absurd*; my objection isn't mechanical/technical.

What bothers me is a feeling that I'm "cheating" when I use this function
that can never be called, in order to "produce" that which I need to
complete my proof.

I wonder if someone could offer a different perspective on this, for
consideration.

Thanks!
-db
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200828/8758d881/attachment.html>