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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-27 18:40:53 -08:00
parent 7f047a95f4
commit 870896ba45
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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