max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix test suite

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-15 15:27:40 -07:00
parent d3b0b49c43
commit c16d4fb926
2 changed files with 120 additions and 120 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/1021.lean.expected.out
View file

@ -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 } }

228
tests/lean/docStr.lean.expected.out
View file

@ -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 } }