unknown identifier 'Implies'

Stream: lean4

[Param Reddy]

Was following https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html

#check Implies gives error saying unknown identifier 'Implies'. Did this get removed and now we have to use -> ?

[Param Reddy]

Similarly getting error with: #check Proof.

[Matt Diamond]

docs#Implies

[Matt Diamond]

it's in Mathlib, you just have to import it (or import a file that imports it)

[Matt Diamond]

not sure about Proof though

[Matt Diamond]

oh wait, Proof isn't real, it's just a hypothetical

[Kyle Miller]

This chapter is a quick "what if we set things up this way".

Click the eyeball icons in the upper-right corners of the code blocks to see the hidden definitions.

[Kyle Miller]

The point of the discussion is that we don't need Implies p q since p → q is the same concept.

[Param Reddy]

Matt Diamond said:

docs#Implies

Just did google search for "lean4 Implies" before posting here and got no links to this doc. Thanks for the pointer.

[Kyle Miller]

Moreover, once we make this identification, the rules for implication show that we can pass back and forth between Implies p q and p → q. In other words, implication between propositions p and q corresponds to having a function that takes any element of p to an element of q. As a result, the introduction of the connective Implies is entirely redundant: we can use the usual function space constructor p → q from dependent type theory as our notion of implication.

[Kyle Miller]

(You're not the first person to ask about this section. It should probably put this conclusion earlier so you're not confused about what Implies is and think it's something you've missed.)

[Param Reddy]

I also should probably read the whole chapter before posting. But yeah if it was not hidden behind the eye, would have been less confused. Thanks for quick answer.