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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2024-02-08 18:04:27 -08:00 • committed by Scott Morrison
parent 61a8695ab1
commit 003835111d
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,8 +1,8 @@
some { range := { pos := { line := 189, column := 42 },
some { range := { pos := { line := 177, column := 42 },
charUtf16 := 42,
endPos := { line := 195, column := 31 },
endPos := { line := 183, column := 31 },
endCharUtf16 := 31 },
selectionRange := { pos := { line := 189, column := 46 },
selectionRange := { pos := { line := 177, column := 46 },
charUtf16 := 46,
endPos := { line := 189, column := 58 },
endPos := { line := 177, column := 58 },
endCharUtf16 := 58 } }

2
tests/lean/run/sharecommon.lean
View file

@ -2,7 +2,7 @@ import Lean.Util.ShareCommon
open Lean.ShareCommon
def check (b : Bool) : ShareCommonT IO Unit := do
unless b do throw $ IO.userError "check failed"
unless b do throw $ IO.userError "check failed"
unsafe def tst1 : ShareCommonT IO Unit := do
let x := [1]