From 870896ba452b634003ab8fa6af577c0adbd169af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Jan 2021 18:40:53 -0800 Subject: [PATCH] chore: fix test --- tests/lean/docStr.lean.expected.out | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out index f1f59dd370..33cf2e2d13 100644 --- a/tests/lean/docStr.lean.expected.out +++ b/tests/lean/docStr.lean.expected.out @@ -190,22 +190,22 @@ g.foo := endPos := { line := 40, column := 47 }, endCharUtf16 := 47 } } optParam := - { range := { pos := { line := 163, column := 13 }, + { range := { pos := { line := 166, column := 13 }, charUtf16 := 13, - endPos := { line := 163, column := 66 }, + endPos := { line := 166, column := 66 }, endCharUtf16 := 66 }, - selectionRange := { pos := { line := 163, column := 17 }, + selectionRange := { pos := { line := 166, column := 17 }, charUtf16 := 17, - endPos := { line := 163, column := 25 }, + endPos := { line := 166, column := 25 }, endCharUtf16 := 25 } } namedPattern := - { range := { pos := { line := 172, column := 13 }, + { range := { pos := { line := 175, column := 13 }, charUtf16 := 13, - endPos := { line := 172, column := 61 }, + endPos := { line := 175, column := 61 }, endCharUtf16 := 61 }, - selectionRange := { pos := { line := 172, column := 17 }, + selectionRange := { pos := { line := 175, column := 17 }, charUtf16 := 17, - endPos := { line := 172, column := 29 }, + endPos := { line := 175, column := 29 }, endCharUtf16 := 29 } } Lean.Meta.forallTelescopeReducing := { range := { pos := { line := 668, column := 0 },