Lean inserts unused variables in an example

Stream: lean4

[Bulhwi Cha]

#eval Lean.versionString -- output: "4.20.0-rc5"

variable (p q r : Prop)

theorem thm0 : p ∧ q ↔ q ∧ p := by
  sorry
/- goal:
p q : Prop ⊢ p ∧ q ↔ q ∧ p
-/

example : p ∧ q ↔ q ∧ p := by
  sorry
/- goal:
p q r : Prop ⊢ p ∧ q ↔ q ∧ p
-/

Lean didn't insert the variable r in the theorem thm0. However, it did in the example above. Was this intended?

[Edward van de Meent]

i suspect it is intended? the change in variable behaviour was done at a point when example already existed, so i'd say so?

[Bulhwi Cha]

This behavior of the variable command makes it hard to predict which variables Lean won't insert into which examples.

[Mario Carneiro]

this is intended

[Bulhwi Cha]

What was the reason behind this decision?

[Mario Carneiro]

the reason for the difference is that def/example has different elaboration behavior from theorem, theorem doesn't let you refer to variables in the body which are not in the statement or included

[Mario Carneiro]

variable (x : Nat)
def foo : Nat := x
example : Nat := x
theorem bar : Nat := x -- unknown identifier 'x'

[Bulhwi Cha]

variable (p : Prop) (x : p)
def foo : p := x
example : p := x
theorem bar : p := x -- unknown identifier 'x'

[Bulhwi Cha]

Let me put it this way: the example command was supposed to behave like the def keyword. Am I correct?

[Bulhwi Cha]

Now I got it. Thanks!

[Jz Pan]

Bulhwi Cha said:

the example command was supposed to behave like the def keyword

Yes, and there exists noncomputable example