## 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: May 08 2021 at 09:11 UTC