variables

Stream: general

[Johan Commelin]

How do I check which variables are in scope in a certain part of a lean file.

[Mario Carneiro]

impossible, I'm afraid

[Kenny Lau]

you can't

[Johan Commelin]

Bleeh

[Ruben Van de Velde]

Who understands lean3 variables?

variables (𝕜)
/-- Expand the square -/
lemma norm_add_sq (x y : E) : ‖x + y‖^2 = ‖x‖^2 + 2 * (re ⟪x, y⟫) + ‖y‖^2 :=
begin
  repeat {rw [sq, ←@inner_self_eq_norm_mul_norm 𝕜]},
  rw [inner_add_add_self, two_mul],
  simp only [add_assoc, add_left_inj, add_right_inj, add_monoid_hom.map_add],
  rw [←inner_conj_symm, conj_re],
end

#check @norm_add_sq
-- norm_add_sq :
--  ∀ {𝕜 : Type u_4} {E : Type u_5} [_inst_1 : is_R_or_C 𝕜] [_inst_2 : normed_add_comm_group E]
--  [_inst_3 : inner_product_space 𝕜 E] (x y : E), ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⇑re (inner x y) + ‖y‖ ^ 2

[Eric Wieser]

This is a quirk in local notation, but you didn't make your mwe in a way that shows it's being used

[Jireh Loreaux]

yeah, this is something I noticed while porting. @Eric Wieser I think when you refactored inner_product_spaceand added these variable (𝕜) lines, a lot of them didn't end up applying because of the local notations present. In Lean 4 I think they work properly though, so I didn't worry about it. (It just made it slightly confusing during porting because suddenly declarations which didn't need an explicit 𝕜 in Lean 3 all of a sudden needed one in Lean 4.)

Ruben, basically, if you do

variable {𝕜 : Type}

local notation my_notation := some_decl 𝕜

variable (𝕜)

lemma foo_involving_my_notation : ... := sorry

then 𝕜 is not explicit in foo_involving_my_notation despite the variable update because of the presence of my_notation, which was declared when 𝕜 was implicit.

[Ruben Van de Velde]

Thanks for the explanation!