error: theorems do not get VM compiled

Stream: new members

[Chinmaya Nagpal]

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]

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]

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]

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.