[Agda] Hanging out with the Lean crowd

[Guillaume Brunerie]

Den mån 24 aug. 2020 kl 10:57 skrev Nils Anders Danielsson <nad at cse.gu.se>:
>
> On 2020-08-23 13:41, Guillaume Brunerie wrote:
> > Den lör 22 aug. 2020 kl 23:21 skrev <mechvel at scico.botik.ru>:
> >> Well, I can write in Agda
> >>
> >> f =
> >>     case  isPrime? (2^(2^(2^1000)) + 7)
> >>     of \
> >>     { (yes _) -> true
> >>     ; (no _)  -> false
> >>     }
> >>
> >> […]
> >>
> >> What is your opinion: is its termination justified?
> >
> > That’s a very interesting question, I’m not really sure what I think
> > about that yet, I have to think more about it.
>
> I thought that your previous message sounded like an argument for
> something like ultrafinitism (which I know little about).

I don’t think I would consider myself an ultrafinitist, but I do find
some of those ideas attractive (even though I don’t know much about
ultrafinitism either).

Best,
Guillaume