Helper functions for Syntax.

These are delayed here to allow some time to bootstrap Array.

def Lean.Syntax.setArgs (stx : Lean.Syntax) (args : Array Lean.Syntax) : Lean.Syntax

Updates the argument list without changing the node kind. Does nothing for non-node nodes.

Equations

• (Lean.Syntax.node info k args_1).setArgs args = Lean.Syntax.node info k args
• stx.setArgs args = stx

def Lean.Syntax.setArg (stx : Lean.Syntax) (i : Nat) (arg : Lean.Syntax) : Lean.Syntax

Updates the i'th argument of the syntax. Does nothing for non-node nodes, or if i is out of bounds of the node list.

Equations

• (Lean.Syntax.node info k args).setArg i arg = Lean.Syntax.node info k (args.setIfInBounds i arg)
• stx.setArg i arg = stx