Local functions in instances

Stream: lean4

[Yuri de Wit]

Want to double check: are (where) local functions supposed to work with instance declarations?
e.g.,

instance : Markup R where
  elem name := (⟨ s!"<{name}{toAttrsString ·}>{toNodesString ·}</{name}>" ⟩)
    where
      toAttrsString (attrs : Array (R .Attr)) : String := attrs.foldl (init := "") (s!"{·} {·}")
      toNodesString (children : Array (R .Node)) : String := children.foldl (init := "") (s!"{.}{.}")

[Leonardo de Moura]

Thanks for reporting. Pushed support for it: https://github.com/leanprover/lean4/commit/fa64c072ab59a100c4596378a1d8e4a9e23abdf1

[Yuri de Wit]

I see that they are associated with the instance and not the method. Even better!