chore: fix tests

This commit is contained in:
Leonardo de Moura 2020-10-05 11:28:52 -07:00
parent fb83e8e79b
commit a6063a5560
3 changed files with 9 additions and 9 deletions

View file

@ -1,12 +1,12 @@
PANIC at f dbgMacros:4:14: unexpected zero
PANIC at g dbgMacros:12:14: unreachable code has been reached
PANIC at h dbgMacros:18:0: assertion violation: x != 0
f2, x: 10
0
9
0
0
0
f2, x: 10
11
g2 started
11

View file

@ -9,10 +9,10 @@ but is expected to have type
failed to synthesize instance
CoeT (PersistentHashMap Nat Nat) m (PersistentHashMap Nat Nat)
phashmap_inst_coherence.lean:12:0: error: application type mismatch
Lean.runEval (sorryAx ?m)
Lean.runEval fun («_» : Unit) => sorryAx ?m
argument
sorryAx ?m
fun («_» : Unit) => sorryAx ?m
has type
?m
Unit → ?m
but is expected to have type
?m
Unit → ?m

View file

@ -11,11 +11,11 @@ protected.lean:28:14: error: unknown identifier 'f'
protected.lean:38:14: error: unknown identifier 'g'
protected.lean:47:6: error: unknown identifier 'g'
protected.lean:47:0: error: application type mismatch
Lean.runEval (sorryAx ?m)
Lean.runEval fun («_» : Unit) => sorryAx ?m
argument
sorryAx ?m
fun («_» : Unit) => sorryAx ?m
has type
?m
Unit → ?m
but is expected to have type
?m
Unit → ?m
8