lean4-htt/tests/lean/1021.lean.expected.out
Kyle Miller ede1acfb44
fix: let anonymous constructor notation elaborate with insufficient arguments (#10391)
This PR gives anonymous constructor notation (`⟨x,y⟩`) an error recovery
mechanism where if there are not enough arguments then synthetic sorries
are inserted for the missing arguments and an error is logged, rather
than outright failing.

Closes #9591.
2025-09-15 16:44:34 +00:00

8 lines
311 B
Text

some
{
range :=
{ pos := { line := 217, column := 0 }, charUtf16 := 0, endPos := { line := 222, column := 31 },
endCharUtf16 := 31 },
selectionRange :=
{ pos := { line := 217, column := 46 }, charUtf16 := 46, endPos := { line := 217, column := 58 },
endCharUtf16 := 58 } }