<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>Hi,</p>
    <p>I'm by no means an expert, but it seems to me that this
      "computational emptyness" of absurd is just corresponding to the
      fact that in constructive logic, you can't have proof by
      contradiction, only proof of negation. That is, at the end absurd
      will always prove a negation. It has type _|_ -> A for some A.
      You will never be able to construct an A with absurd, only ever
      its negation.</p>
    <p>Manuel<br>
    </p>
    <div class="moz-cite-prefix">On 28.08.20 15:11, David Banas wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CADz=fO2A8gX0WikLvyp3XVx2zxxsRWERzCkCK_M1SavMPQczgA@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <div dir="ltr">Hi all,<br>
        <div><br>
        </div>
        <div>I'm brand new to Agda and the Curry-Howard isomorphism (and
          really loving this new exploration of both!), and I have a <i>philosophical</i>
          objection to how the <font face="monospace"><b>absurd</b></font>
          function is used to generate whatever we need to complete a
          proof.</div>
        <div><br>
        </div>
        <div>I understand how we are able to satisfy the Agda compiler
          with the definition of <font face="monospace"><b>absurd</b></font>;
          my objection isn't mechanical/technical.</div>
        <div><br>
        </div>
        <div>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.</div>
        <div><br>
        </div>
        <div>I wonder if someone could offer a different perspective on
          this, for consideration.</div>
        <div><br>
        </div>
        <div>Thanks!</div>
        <div>-db</div>
        <div><br>
        </div>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
  </body>
</html>