symbol is missing from vscode outline

Stream: general

[fonqL]

vscode version: 1.84.2

open Nat in
def x := 0

set_option pp.all true in
def y := 0

x and y can't be shown in vscode outline.
behavior:

[Marc Huisinga]

fonqL said:

vscode version: 1.84.2

open Nat in
def x := 0

set_option pp.all true in
def y := 0

x and y can't be shown in vscode outline.
behavior:

Could you create a GitHub issue at https://github.com/leanprover/lean4/issues for this?

[fonqL]

Sorry for the late reply.
4655