Implies operation

Stream: general

[Greg Shuflin]

I'm going through _Theorem Proving in Lean_ right now and encountered:
https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html

#check And     -- Prop → Prop → Prop
#check Or      -- Prop → Prop → Prop
#check Not     -- Prop → Prop
#check Implies -- Prop → Prop → Prop

I'm getting an unknown identifier "Implies" error here when I try this on my own system - does this mean that Implies should be in some prelude just as the more basic logical operations are, and something about my setup is broken? Or is it not and is the text of _Theorem Proving in Lean_ incorrect?

[Greg Shuflin]

It looks like Proof is also assumed to be in scope by this documentation, but that isn't happening on my system.

Also, this documentation introduces an axiom keyword - should I expect to see this documented in https://lean-lang.org/doc/reference/latest/# ?

[Matt Diamond]

Implies throws a lot of people off... if you click the eye symbol on the upper right of the code box, it will show you what's really going on:
image.png

[Matt Diamond]

it's defined specifically for that example... it's not something you actually need/use, and the text will eventually explain that

[Greg Shuflin]

ah okay I didn't realize what the eye icon was doing

[Matt Diamond]

yep... and if you click it for the next block, you'll see where Proof is coming from:
image.png

[Greg Shuflin]

what about axiom? and theorem? those look like language keywords not defined names

[Matt Diamond]

yeah those are legitimate keywords... I don't know where the docs explain them

[Matt Diamond]

the tutorial that you're reading should address those

[Greg Shuflin]

it looks like it explains them more later on, yeah. still it would be nice if there was an authortiative list of every language keyword in lean somewhere

[Ruben Van de Velde]

I imagine the reference manual will eventually have something like that, for the built-in keywords at least

[Mario Carneiro]

This section is frequently misread, but it's explaining not how lean works but how lean could work, i.e. an alternative way of setting things up. That's why not all of the constants it references actually exist in core lean

[Patrick Massot]

@Jeremy Avigad It’s true that we get this question rather often. Maybe it’s worth the trouble of adding one warning sentence on top of that “could”?

[Jeremy Avigad]

Yes, I'll make a round of revisions soon and try to clarify.