elaborate rwRule

Stream: lean4

[Moritz Doll]

Is there a function that elaborates a rwRule such that it can be easily be stuffed into Lean.MVarId.rewrite? Somewhat related I don't understand why the whole Lean.Elab.Tactic.Rewrite uses Syntax instead of TSyntax. Is this for bootstrapping reasons or are there any big advantages of Syntax over TSyntax?

[Sebastian Ullrich]

Many files have not been ported to TSyntax yet