Zulip Chat Archive

Stream: new members

Topic: VS Code help

Ben Toner (Jul 28 2021 at 09:11):

When looking at this lemma in VS Code, is there a way to jump to the definition of (re_clm : 𝕜 →L[ℝ] ℝ).times_cont_diff? When I hover or use the "Go to Definition" command, it takes me to the definition of exact.

lemma times_cont_diff_norm_sq : times_cont_diff  n (λ x : E, x ^ 2) :=
  simp only [sq,  inner_self_eq_norm_sq],
  exact (re_clm : 𝕜 L[] ).times_cont_diff.comp (times_cont_diff_id.inner times_cont_diff_id)

Eric Wieser (Jul 28 2021 at 09:12):

You can sometimes get around this by putting the expression in a have := ... first

Eric Wieser (Jul 28 2021 at 09:12):

Failing that, #check always behaves

Ben Toner (Jul 28 2021 at 09:15):

@Eric Wieser Thanks, #check works.

Last updated: Dec 20 2023 at 11:08 UTC