Expression render round-trips

Successfully parsed expressions render to canonical source that parses back to the same rendered token sequence.

def TorchLean.Tensor.Internal.Syntax.parseExpression (source : String) (config : ExpressionConfig := ExpressionConfig.transformation) (policy : IdentifierPolicy := IdentifierPolicy.pythonUnicode) : Result Expression

Parse one side of a transformation pattern.

theorem TorchLean.Tensor.Internal.Syntax.parseExpression_render_eq_ok (source : String) (config : ExpressionConfig) (expression : Expression) (hParse : parseExpression source config = Except.ok expression) : Except.map Expression.render (parseExpression expression.render config) = Except.ok expression.render

Parsing a successful expression's canonical rendering succeeds with the same canonical syntax.

The reparsed tree has fresh source spans and fresh anonymous-axis occurrence offsets. Comparing renderings captures every parser distinction used by later checking while intentionally ignoring that source-location metadata.