Lean 4 'unknown identifier Proof'

Question

I have been experiencing an issue when using Lean 4.

I ran into it while working my way through the docs, in the Propositions and Proofs section. Under Propositions as Types, the docs introduce the Proof Type:

We could then introduce, for each element p : Prop, another type Proof p, for the type of proofs of p.

Below, it shows a code snippet checking for the type of Proof, which returns Proof : Prop → Type:

#check Proof   -- Proof : Prop → Type

When I try running this snippet, I get the following error:

example.lean:3:7: error: unknown identifier 'Proof'

implying that lean can not find the Proof type. This is my problem, how do I get Lean to recognize Proof?

Thanks!

Answer 1

There is no such type called Proof. The docs mention it as an example of how Lean could have been implemented, but go on to explain why it was not implemented like that.