<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Aug 20, 2020 at 10:29 PM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Probably the majority of people keep in mind a bit another thing:<br>
   a possibility to use a non-constructive proof, when failed to provide<br>
   a constructive one.<br>
<br>
Does Agda support such a possibility?<br></blockquote><div><br></div><div>Everything you do in Agda is constructive by default, but you can always use `postulate` to add any non-constructive principle you want. It will not (or at least, should not) break Agda in any way, except that you (obviously) lose canonicity, i.e. you may have a `b : Bool` that does not evaluate to `true` or `false`.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

I cannot imagine: what can be wrong in this discourse.<br>
In what way can it be possible the result R different from (1) and (2).<br>
How may it look this R ?<br>
The result of (1) or (2) exists in nature independently on whether we <br>
have shown<br>
some witness or not.<br>
?<br></blockquote><div><br></div><div>There is nothing inherently wrong with either constructive or non-constructive mathematics, which one you use depends on what job you want to use it for. In particular, the meaning of the word 'exists' is not the same in constructive and non-constructive mathematics. What can be annoying are the people who are convinced non-constructive mathematics is the right tool for *every* job.<br></div><div><br></div><div>-- Jesper<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
--<br>
SM<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div></div>