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

fix: declaration ranges changed after stage0 update (#5845)

Browse source 
Recently declaration ranges have changed slightly to include attribute
lists. Fixes a test that broke.
This commit is contained in:
Kyle Miller 2024-10-25 14:38:06 -07:00 • committed by GitHub
parent f292184642
commit abe6d5bca7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,7 +1,7 @@
some
{
range :=
{ pos := { line := 202, column := 42 }, charUtf16 := 42, endPos := { line := 208, column := 31 },
{ pos := { line := 202, column := 0 }, charUtf16 := 0, endPos := { line := 208, column := 31 },
endCharUtf16 := 31 },
selectionRange :=
{ pos := { line := 202, column := 46 }, charUtf16 := 46, endPos := { line := 202, column := 58 },