Stream: new members
Keeley Hoek (Nov 12 2018 at 11:55):
How can you ask lean to decide something which is decidable? e.g.
Kevin Buzzard (Nov 12 2018 at 12:02):
dec_trivial will do it in theory, but for primes it might well time out in practice and you're better off using
Keeley Hoek (Nov 12 2018 at 12:04):
ok thanks Kevin
Last updated: May 08 2021 at 09:11 UTC