<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Ah, thank you; that helps.<div class="">Sort of a back-propagation of absurdity, as it were?</div><div class="">If something is calling <font face="Menlo" class="">absurd</font>, then it must be absurd, as well; is that it?</div><div class=""><br class=""></div><div class="">Thanks!</div><div class="">-db</div><div class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Aug 28, 2020, at 7:05 AM, Nicolas Pouillard <<a href="mailto:nicolas.pouillard+agda@gmail.com" class="">nicolas.pouillard+agda@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hi,<div class=""><br class=""></div><div class="">One way to understand that you are not cheating when you pass an argument to <b class="">absurd </b>is to realise that this piece of code is already unreachable.</div><div class="">Syntactically it seems that one could reach this part of the code with input values. However the whole system is designed such that it is not possible.</div><div class=""><br class=""></div><div class="">Nicolas</div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Aug 28, 2020 at 3:29 PM Manuel Bärenz <<a href="mailto:manuel@enigmage.de" class="">manuel@enigmage.de</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div class=""><p class="">Hi,</p><p class="">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 class="">Manuel<br class="">
</p>
<div class="">On 28.08.20 15:11, David Banas wrote:<br class="">
</div>
<blockquote type="cite" class="">
<div dir="ltr" class="">Hi all,<br class="">
<div class=""><br class="">
</div>
<div class="">I'm brand new to Agda and the Curry-Howard isomorphism (and
really loving this new exploration of both!), and I have a <i class="">philosophical</i>
objection to how the <font face="monospace" class=""><b class="">absurd</b></font>
function is used to generate whatever we need to complete a
proof.</div>
<div class=""><br class="">
</div>
<div class="">I understand how we are able to satisfy the Agda compiler
with the definition of <font face="monospace" class=""><b class="">absurd</b></font>;
my objection isn't mechanical/technical.</div>
<div class=""><br class="">
</div>
<div class="">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 class=""><br class="">
</div>
<div class="">I wonder if someone could offer a different perspective on
this, for consideration.</div>
<div class=""><br class="">
</div>
<div class="">Thanks!</div>
<div class="">-db</div>
<div class=""><br class="">
</div>
</div>
<br class="">
<fieldset class=""></fieldset>
<pre class="">_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</div>
_______________________________________________<br class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class="">
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">
</blockquote></div>
_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></div></body></html>