Elaborating a InductiveView

Stream: Is there code for X?

[William Sørensen]

elabInductiveViews has been private'd now, the only way to elab one now is to provide a Syntax by the looks of it. Is there a method like this implemented:

def InductiveView.toTSyntax [Monad m] [MonadQuotation m] (vw : InductiveView) : m $ TSyntax ``Lean.Parser.Command.declaration := do

?