Hello

Inspecting Lean

#eval
"4.8.0-rc1"
 
Lean.versionString: String
Lean.versionString

#eval
"4.8.0"
 
Lean.versionStringCore: String
Lean.versionStringCore

#eval
"leanprover/lean4:4.8.0-rc1"
 
Lean.toolchain: String
Lean.toolchain

#eval
"leanprover/lean4"
 
Lean.origin: String
Lean.origin

#eval
"dcccfb73cb247e9478220375ab7de03f7c67e505"
 
Lean.githash: String
Lean.githash

Proofs

theorem 
test: ∀ (p q : Prop), p → q → (p ∧ q ↔ q ∧ p)
test (
p: Prop
p 
q: Prop
q : 
Prop: Type
Prop) (
hp: p
hp : 
p: Prop
p) (
hq: q
hq : 
q: Prop
q): 
p: Prop
p ∧ 
q: Prop
q ↔ 
q: Prop
q ∧ 
p: Prop
p := by
Goals accomplished! 🐙
  apply 
Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.intro
p, q: Prop
hp: p
hq: q
mp
p ∧ q → q ∧ p
p, q: Prop
hp: p
hq: q
mpr
q ∧ p → p ∧ q
  .
p, q: Prop
hp: p
hq: q
mp
p ∧ q → q ∧ p intro
p, q: Prop
hp: p
hq: q
mp
p ∧ q → q ∧ p 
h: p ∧ q
h
Warning: unused variable `h`
note: this linter can be disabled with `set_option linter.unusedVariables false`
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp
q ∧ p
    apply 
And.intro: ∀ {a b : Prop}, a → b → a ∧ b
And.intro
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.left
q
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.right
p
    .
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.left
q exact 
hq: q
hq
Goals accomplished! 🐙
    .
p, q: Prop
hp: p
hq: q
h: p ∧ q
mp.right
p exact 
hp: p
hp
Goals accomplished! 🐙
  .
p, q: Prop
hp: p
hq: q
mpr
q ∧ p → p ∧ q intro
p, q: Prop
hp: p
hq: q
mpr
q ∧ p → p ∧ q 
h: q ∧ p
h
Warning: unused variable `h`
note: this linter can be disabled with `set_option linter.unusedVariables false`
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr
p ∧ q
    apply 
And.intro: ∀ {a b : Prop}, a → b → a ∧ b
And.intro
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.left
p
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.right
q
    .
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.left
p exact 
hp: p
hp
Goals accomplished! 🐙
    .
p, q: Prop
hp: p
hq: q
h: q ∧ p
mpr.right
q exact 
hq: q
hq
Goals accomplished! 🐙