Zulip Chat Archive

Stream: general

Topic: variables


Johan Commelin (May 28 2018 at 10:50):

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

Mario Carneiro (May 28 2018 at 10:50):

impossible, I'm afraid

Kenny Lau (May 28 2018 at 10:50):

you can't

Johan Commelin (May 28 2018 at 10:50):

Bleeh

Ruben Van de Velde (Jun 06 2023 at 14:21):

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 (Jun 06 2023 at 14:22):

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 (Jun 06 2023 at 14:34):

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 (Jun 06 2023 at 15:21):

Thanks for the explanation!


Last updated: Dec 20 2023 at 11:08 UTC