Theorems

Stream: general

[Guillermo Barajas Ayuso]

Hi guys do you know how types can somehow be theorems? E.g. strong_indefinite_description in classical.

[Mario Carneiro]

There is nothing preventing you from marking a type as a theorem, or a prop as a def

[Mario Carneiro]

Usually we stick to theorem or lemma for things in Prop and def for things in Sort or Type, though, for a few reasons. The VM will not generate code for theorems, and this will affect downstream definitions as well, so that is one reason; it is not a problem with strong_indefinite_description because this theorem is not computable anyway. Also a theorem is never unfolded, which is almost never necessary for a Prop because of proof irrelevance but is often important for defs since we may want to prove theorems about the def later. Here it is not a problem in strong_indefinite_description because the definition is supposed to be arbitrary in its type, so unfolding should never be necessary.

[Guillermo Barajas Ayuso]

Ok that makes sense, thanks a lot!