Classical unknown identifier 'not_imp'

Stream: new members

[Spearman]

I was able to access Classical.em, but for some reason 'not_imp' gives me the error error: unknown identifier 'not_imp'

open Classical
#check em
#check not_imp

info: [0/2] Building Main
error: > LEAN_PATH=./.lake/build/lib LD_LIBRARY_PATH=./.lake/build/lib /home/spearman/.elan/toolchains/stable/bin/lean ./././Main.lean -R ././. -o ./.lake/build/lib/Main.olean -i ./.lake/build/lib/Main.ilean -c ./.lake/build/ir/Main.c
error: stdout:
Classical.em (p : Prop) : p ∨ ¬p
./././Main.lean:3:7: error: unknown identifier 'not_imp'
error: external command `/home/spearman/.elan/toolchains/stable/bin/lean` exited with code 1

[Henrik Böving]

That's gonna need more information on your setup to debug, it works in the browser version: https://live.lean-lang.org/#code=open%20Classical%0A%0A%23check%20not_imp . What Lean version are you running?

[Spearman]

Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)

[Kyle Miller]

Classical.not_imp is in 4.8.0, and not_imp needs you to import Mathlib.Logic.Basic

[Spearman]

I was able to update now to 4.8.0 and use 'not_imp'.

I'm confused though, because I have to 'import Init.Classical' or 'open Classical' to access em, but I don't have to import or open Classical to access not_imp:

#check em
#check not_imp

✖ [1/3] Building Main
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH=././.lake/build/lib /home/spearman/.elan/toolchains/stable/bin/lean ././././Main.lean -R ./././. -o ././.lake/build/lib/Main.olean -i ././.lake/build/lib/Main.ilean -c ././.lake/build/ir/Main.c --json
error: ././././Main.lean:1:7: unknown identifier 'em'
info: ././././Main.lean:2:0: Classical.not_imp {a b : Prop} : ¬(a → b) ↔ a ∧ ¬b
error: Lean exited with code 1

[Kyle Miller]

When you do open Classical it makes it so you can refer to Classical.em as em for short.

not_imp is also short for Classical.not_imp, but there's an export line that makes it permanently able to be referred to without qualification. The command is making it so that it's like open Classical (not_imp) is automatically at the top of every file.