# Zulip Chat Archive

## Stream: new members

### Topic: error: theorems do not get VM compiled

#### Chinmaya Nagpal (Sep 12 2023 at 11:27):

I'm not sure how to interpret this error message: `theorems do not get VM compiled, use 'def' or add 'noncomputable' modifier to 'thm1'.`

Encountered when trying to show that `bool`

and `nat`

are inhabited types, suggested as an exercise in chapter 7 of TPIL3.

```
theorem thm1 : inhabited(bool) := inhabited.mk(tt)
theorem thm2 : inhabited(nat) := inhabited.mk(nat.zero)
```

Is this because the result of the theorem is not a proposition?

New here, so not sure if this is the correct place to post this problem. Thanks in advance for any help.

#### Riccardo Brasca (Sep 12 2023 at 11:32):

`inhabited`

contains data (meaning that it remembers the element you choose), so it should be a `def`

. May I suggest you to switch to Lean4? There is essentially no point in still using Lean3 today.

#### Kevin Buzzard (Sep 12 2023 at 11:37):

PS yes this is the correct place to ask questions like this -- feel free to ask more. You need to decide whether you're proving a theorem or making a definition. We have docs#Nonempty for the `Prop`

version -- this would then be a theorem. Hopefully the docstring for Nonempty helps clarify things.

#### Kyle Miller (Sep 12 2023 at 12:03):

Chinmaya Nagpal said:

Is this because the result of the theorem is not a proposition?

Exactly -- the error message (once you know it's meaning) is telling you that you're accidentally making a definition you can't `#eval`

. The Prop version of the predicate is `nonempty`

.

Last updated: Dec 20 2023 at 11:08 UTC