chore: remove volatile cases from test
This commit is contained in:
parent
f645429df4
commit
0d86ebe5eb
2 changed files with 0 additions and 30 deletions
|
|
@ -98,8 +98,5 @@ def printRangesTest : MetaM Unit := do
|
|||
printRanges `f.foo
|
||||
printRanges `g
|
||||
printRanges `g.foo
|
||||
printRanges `optParam
|
||||
printRanges `namedPattern
|
||||
printRanges `Lean.Meta.forallTelescopeReducing
|
||||
|
||||
#eval printRangesTest
|
||||
|
|
|
|||
|
|
@ -189,30 +189,3 @@ g.foo :=
|
|||
charUtf16 := 44,
|
||||
endPos := { line := 40, column := 47 },
|
||||
endCharUtf16 := 47 } }
|
||||
optParam :=
|
||||
{ range := { pos := { line := 152, column := 13 },
|
||||
charUtf16 := 13,
|
||||
endPos := { line := 152, column := 66 },
|
||||
endCharUtf16 := 66 },
|
||||
selectionRange := { pos := { line := 152, column := 17 },
|
||||
charUtf16 := 17,
|
||||
endPos := { line := 152, column := 25 },
|
||||
endCharUtf16 := 25 } }
|
||||
namedPattern :=
|
||||
{ range := { pos := { line := 161, column := 13 },
|
||||
charUtf16 := 13,
|
||||
endPos := { line := 161, column := 61 },
|
||||
endCharUtf16 := 61 },
|
||||
selectionRange := { pos := { line := 161, column := 17 },
|
||||
charUtf16 := 17,
|
||||
endPos := { line := 161, column := 29 },
|
||||
endCharUtf16 := 29 } }
|
||||
Lean.Meta.forallTelescopeReducing :=
|
||||
{ range := { pos := { line := 699, column := 0 },
|
||||
charUtf16 := 0,
|
||||
endPos := { line := 700, column := 58 },
|
||||
endCharUtf16 := 58 },
|
||||
selectionRange := { pos := { line := 699, column := 4 },
|
||||
charUtf16 := 4,
|
||||
endPos := { line := 699, column := 27 },
|
||||
endCharUtf16 := 27 } }
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue