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-12 08:14:16 -08:00
parent b6abf19656
commit 42b5e780f5
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -82,5 +82,5 @@ namedPattern :=
{ range := { pos := { line := 166, column := 13 }, endPos := { line := 166, column := 61 } },
selectionRange := { pos := { line := 166, column := 17 }, endPos := { line := 166, column := 29 } } }
Lean.Meta.forallTelescopeReducing :=
{ range := { pos := { line := 663, column := 0 }, endPos := { line := 664, column := 58 } },
selectionRange := { pos := { line := 663, column := 4 }, endPos := { line := 663, column := 27 } } }
{ range := { pos := { line := 668, column := 0 }, endPos := { line := 669, column := 58 } },
selectionRange := { pos := { line := 668, column := 4 }, endPos := { line := 668, column := 27 } } }