[Agda] Hanging out with the Lean crowd

mechvel at scico.botik.ru mechvel at scico.botik.ru
Sat Aug 22 20:49:20 CEST 2020


On 2020-08-22 21:39, mechvel at scico.botik.ru wrote:
> [..]

> I say "unsafe usage" because there also is a safe usage of EM - when
> the predicate P is solvable.

Corrrection:
I meant "the related predicate". Wile in the example with Nat, this 
predicate is
(exists n such that P n), and it is not solved.

--
SM


More information about the Agda mailing list