[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-30 00:26, mechvel at scico.botik.ru wrote:
> On 2020-08-23 00:21, mechvel at scico.botik.ru wrote:
>> [..]
> 
> So that if something can be proved without using excluded middle, it
> is desirable to do this.

I would also add:
the results that can be proved without using excluded middle constitute 
may be
1/30 of essential results in mathematics.
But this 1/30 is still a large piece.

Regards,

------
Sergei