[Agda] Hanging out with the Lean crowd

[Jesper Cockx]

On Thu, Aug 20, 2020 at 10:29 PM <mechvel at scico.botik.ru> wrote:

> Probably the majority of people keep in mind a bit another thing:
>    a possibility to use a non-constructive proof, when failed to provide
>    a constructive one.
>
> Does Agda support such a possibility?
>

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`.


> I cannot imagine: what can be wrong in this discourse.
> In what way can it be possible the result R different from (1) and (2).
> How may it look this R ?
> The result of (1) or (2) exists in nature independently on whether we
> have shown
> some witness or not.
> ?
>

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.

-- Jesper


>
> --
> SM
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200820/6577b6d0/attachment.html>