[Agda] Hanging out with the Lean crowd

[Nils Anders Danielsson]

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

-- 
/NAD