Zulip Chat Archive
Stream: new members
Topic: decidability
Keeley Hoek (Nov 12 2018 at 11:55):
How can you ask lean to decide something which is decidable? e.g. prime n
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 norm_num
Keeley Hoek (Nov 12 2018 at 12:04):
ok thanks Kevin
Last updated: Dec 20 2023 at 11:08 UTC