fix(frontends/lean/parser): start positions of trailing parser (NuD) nodes

[digama0]

As observed by @eric-wieser , the node for notation[$] in

theorem foo : true :=
id $ trivial

was covering only the span $ trivial instead of id $ trivial, meaning that the id child is outside of the span of its parent node. The fix is to take the start position from the start position of the first child instead of the current parser position when we parse a trailing node. (We also want to use this position for most other activities like constructing multiple expressions all with the same position due to notation expansion, but not for the error message when the parse is invalid.)

[eric-wieser]

CI seems unhappy with this test:

lean/tests/lean/interactive/info.lean

Lines 15 to 16 in cb0da9f

	example := [tt]++[]
	--^ "command": "info"

which no longer produces

lean/tests/lean/interactive/info.lean.expected.out

Line 8 in cb0da9f

{"record":{"full-id":"has_append.append","source":,"state":"⊢ list bool","type":"Π {α : Type} [self : has_append α], α → α → α"},"response":"ok","seq_num":16}

[eric-wieser]

I don't understand this change; I'm probably blind, but it appears that nothing uses p below any more?