From c16d4fb92652cbd09c59b74adfa8db52a03cd30f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Sep 2022 15:27:40 -0700 Subject: [PATCH] chore: fix test suite --- tests/lean/1021.lean.expected.out | 12 +- tests/lean/docStr.lean.expected.out | 228 ++++++++++++++-------------- 2 files changed, 120 insertions(+), 120 deletions(-) diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out index ef76cce863..df9bb7a16d 100644 --- a/tests/lean/1021.lean.expected.out +++ b/tests/lean/1021.lean.expected.out @@ -1,8 +1,8 @@ some { range := { pos := { line := 134, column := 41 }, - charUtf16 := 41, - endPos := { line := 140, column := 31 }, - endCharUtf16 := 31 }, + charUtf16 := 41, + endPos := { line := 140, column := 31 }, + endCharUtf16 := 31 }, selectionRange := { pos := { line := 134, column := 45 }, - charUtf16 := 45, - endPos := { line := 134, column := 57 }, - endCharUtf16 := 57 } } + charUtf16 := 45, + endPos := { line := 134, column := 57 }, + endCharUtf16 := 57 } } diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out index 86c95af432..2a3987f5fc 100644 --- a/tests/lean/docStr.lean.expected.out +++ b/tests/lean/docStr.lean.expected.out @@ -20,172 +20,172 @@ doc string for 'g' is not available "Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues bulding the telescope if it is a `forall`. " Foo := { range := { pos := { line := 4, column := 0 }, - charUtf16 := 0, - endPos := { line := 6, column := 58 }, - endCharUtf16 := 58 }, + charUtf16 := 0, + endPos := { line := 6, column := 58 }, + endCharUtf16 := 58 }, selectionRange := { pos := { line := 4, column := 10 }, - charUtf16 := 10, - endPos := { line := 4, column := 13 }, - endCharUtf16 := 13 } } + charUtf16 := 10, + endPos := { line := 4, column := 13 }, + endCharUtf16 := 13 } } Foo.name := { range := { pos := { line := 5, column := 19 }, - charUtf16 := 19, - endPos := { line := 5, column := 23 }, - endCharUtf16 := 23 }, + charUtf16 := 19, + endPos := { line := 5, column := 23 }, + endCharUtf16 := 23 }, selectionRange := { pos := { line := 5, column := 19 }, - charUtf16 := 19, - endPos := { line := 5, column := 23 }, - endCharUtf16 := 23 } } + charUtf16 := 19, + endPos := { line := 5, column := 23 }, + endCharUtf16 := 23 } } Foo.val := { range := { pos := { line := 6, column := 44 }, - charUtf16 := 44, - endPos := { line := 6, column := 47 }, - endCharUtf16 := 47 }, + charUtf16 := 44, + endPos := { line := 6, column := 47 }, + endCharUtf16 := 47 }, selectionRange := { pos := { line := 6, column := 44 }, - charUtf16 := 44, - endPos := { line := 6, column := 47 }, - endCharUtf16 := 47 } } + charUtf16 := 44, + endPos := { line := 6, column := 47 }, + endCharUtf16 := 47 } } myAxiom := { range := { pos := { line := 9, column := 0 }, - charUtf16 := 0, - endPos := { line := 9, column := 19 }, - endCharUtf16 := 19 }, + charUtf16 := 0, + endPos := { line := 9, column := 19 }, + endCharUtf16 := 19 }, selectionRange := { pos := { line := 9, column := 6 }, - charUtf16 := 6, - endPos := { line := 9, column := 13 }, - endCharUtf16 := 13 } } + charUtf16 := 6, + endPos := { line := 9, column := 13 }, + endCharUtf16 := 13 } } Boo := { range := { pos := { line := 11, column := 0 }, - charUtf16 := 0, - endPos := { line := 15, column := 12 }, - endCharUtf16 := 12 }, + charUtf16 := 0, + endPos := { line := 15, column := 12 }, + endCharUtf16 := 12 }, selectionRange := { pos := { line := 11, column := 10 }, - charUtf16 := 10, - endPos := { line := 11, column := 13 }, - endCharUtf16 := 13 } } + charUtf16 := 10, + endPos := { line := 11, column := 13 }, + endCharUtf16 := 13 } } Boo.makeBoo := { range := { pos := { line := 13, column := 2 }, - charUtf16 := 2, - endPos := { line := 13, column := 9 }, - endCharUtf16 := 9 }, + charUtf16 := 2, + endPos := { line := 13, column := 9 }, + endCharUtf16 := 9 }, selectionRange := { pos := { line := 13, column := 2 }, - charUtf16 := 2, - endPos := { line := 13, column := 9 }, - endCharUtf16 := 9 } } + charUtf16 := 2, + endPos := { line := 13, column := 9 }, + endCharUtf16 := 9 } } Boo.x := { range := { pos := { line := 14, column := 27 }, - charUtf16 := 27, - endPos := { line := 14, column := 28 }, - endCharUtf16 := 28 }, + charUtf16 := 27, + endPos := { line := 14, column := 28 }, + endCharUtf16 := 28 }, selectionRange := { pos := { line := 14, column := 27 }, - charUtf16 := 27, - endPos := { line := 14, column := 28 }, - endCharUtf16 := 28 } } + charUtf16 := 27, + endPos := { line := 14, column := 28 }, + endCharUtf16 := 28 } } Boo.y := { range := { pos := { line := 15, column := 4 }, - charUtf16 := 4, - endPos := { line := 15, column := 5 }, - endCharUtf16 := 5 }, + charUtf16 := 4, + endPos := { line := 15, column := 5 }, + endCharUtf16 := 5 }, selectionRange := { pos := { line := 15, column := 4 }, - charUtf16 := 4, - endPos := { line := 15, column := 5 }, - endCharUtf16 := 5 } } + charUtf16 := 4, + endPos := { line := 15, column := 5 }, + endCharUtf16 := 5 } } Tree := { range := { pos := { line := 18, column := 0 }, - charUtf16 := 0, - endPos := { line := 20, column := 56 }, - endCharUtf16 := 56 }, + charUtf16 := 0, + endPos := { line := 20, column := 56 }, + endCharUtf16 := 56 }, selectionRange := { pos := { line := 18, column := 10 }, - charUtf16 := 10, - endPos := { line := 18, column := 14 }, - endCharUtf16 := 14 } } + charUtf16 := 10, + endPos := { line := 18, column := 14 }, + endCharUtf16 := 14 } } Tree.rec := { range := { pos := { line := 18, column := 0 }, - charUtf16 := 0, - endPos := { line := 20, column := 56 }, - endCharUtf16 := 56 }, + charUtf16 := 0, + endPos := { line := 20, column := 56 }, + endCharUtf16 := 56 }, selectionRange := { pos := { line := 18, column := 10 }, - charUtf16 := 10, - endPos := { line := 18, column := 14 }, - endCharUtf16 := 14 } } + charUtf16 := 10, + endPos := { line := 18, column := 14 }, + endCharUtf16 := 14 } } Tree.casesOn := { range := { pos := { line := 18, column := 0 }, - charUtf16 := 0, - endPos := { line := 20, column := 56 }, - endCharUtf16 := 56 }, + charUtf16 := 0, + endPos := { line := 20, column := 56 }, + endCharUtf16 := 56 }, selectionRange := { pos := { line := 18, column := 10 }, - charUtf16 := 10, - endPos := { line := 18, column := 14 }, - endCharUtf16 := 14 } } + charUtf16 := 10, + endPos := { line := 18, column := 14 }, + endCharUtf16 := 14 } } Tree.node := { range := { pos := { line := 19, column := 2 }, - charUtf16 := 2, - endPos := { line := 19, column := 64 }, - endCharUtf16 := 64 }, + charUtf16 := 2, + endPos := { line := 19, column := 64 }, + endCharUtf16 := 64 }, selectionRange := { pos := { line := 19, column := 35 }, - charUtf16 := 35, - endPos := { line := 19, column := 39 }, - endCharUtf16 := 39 } } + charUtf16 := 35, + endPos := { line := 19, column := 39 }, + endCharUtf16 := 39 } } Tree.leaf := { range := { pos := { line := 20, column := 2 }, - charUtf16 := 2, - endPos := { line := 20, column := 56 }, - endCharUtf16 := 56 }, + charUtf16 := 2, + endPos := { line := 20, column := 56 }, + endCharUtf16 := 56 }, selectionRange := { pos := { line := 20, column := 39 }, - charUtf16 := 39, - endPos := { line := 20, column := 43 }, - endCharUtf16 := 43 } } + charUtf16 := 39, + endPos := { line := 20, column := 43 }, + endCharUtf16 := 43 } } Bla.test := { range := { pos := { line := 25, column := 0 }, - charUtf16 := 0, - endPos := { line := 31, column := 16 }, - endCharUtf16 := 16 }, + charUtf16 := 0, + endPos := { line := 31, column := 16 }, + endCharUtf16 := 16 }, selectionRange := { pos := { line := 25, column := 4 }, - charUtf16 := 4, - endPos := { line := 25, column := 8 }, - endCharUtf16 := 8 } } + charUtf16 := 4, + endPos := { line := 25, column := 8 }, + endCharUtf16 := 8 } } Bla.test.aux := { range := { pos := { line := 31, column := 2 }, - charUtf16 := 2, - endPos := { line := 31, column := 16 }, - endCharUtf16 := 16 }, + charUtf16 := 2, + endPos := { line := 31, column := 16 }, + endCharUtf16 := 16 }, selectionRange := { pos := { line := 31, column := 2 }, - charUtf16 := 2, - endPos := { line := 31, column := 5 }, - endCharUtf16 := 5 } } + charUtf16 := 2, + endPos := { line := 31, column := 5 }, + endCharUtf16 := 5 } } f := { range := { pos := { line := 35, column := 0 }, - charUtf16 := 0, - endPos := { line := 39, column := 14 }, - endCharUtf16 := 14 }, + charUtf16 := 0, + endPos := { line := 39, column := 14 }, + endCharUtf16 := 14 }, selectionRange := { pos := { line := 35, column := 4 }, - charUtf16 := 4, - endPos := { line := 35, column := 5 }, - endCharUtf16 := 5 } } + charUtf16 := 4, + endPos := { line := 35, column := 5 }, + endCharUtf16 := 5 } } f.foo := { range := { pos := { line := 36, column := 44 }, - charUtf16 := 44, - endPos := { line := 38, column := 22 }, - endCharUtf16 := 22 }, + charUtf16 := 44, + endPos := { line := 38, column := 22 }, + endCharUtf16 := 22 }, selectionRange := { pos := { line := 36, column := 44 }, - charUtf16 := 44, - endPos := { line := 36, column := 47 }, - endCharUtf16 := 47 } } + charUtf16 := 44, + endPos := { line := 36, column := 47 }, + endCharUtf16 := 47 } } g := { range := { pos := { line := 41, column := 0 }, - charUtf16 := 0, - endPos := { line := 45, column := 7 }, - endCharUtf16 := 7 }, + charUtf16 := 0, + endPos := { line := 45, column := 7 }, + endCharUtf16 := 7 }, selectionRange := { pos := { line := 41, column := 4 }, - charUtf16 := 4, - endPos := { line := 41, column := 5 }, - endCharUtf16 := 5 } } + charUtf16 := 4, + endPos := { line := 41, column := 5 }, + endCharUtf16 := 5 } } g.foo := { range := { pos := { line := 42, column := 44 }, - charUtf16 := 44, - endPos := { line := 44, column := 22 }, - endCharUtf16 := 22 }, + charUtf16 := 44, + endPos := { line := 44, column := 22 }, + endCharUtf16 := 22 }, selectionRange := { pos := { line := 42, column := 44 }, - charUtf16 := 44, - endPos := { line := 42, column := 47 }, - endCharUtf16 := 47 } } + charUtf16 := 44, + endPos := { line := 42, column := 47 }, + endCharUtf16 := 47 } }