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

chore(tests/lean/inst_error.lean.expected.out): fix output

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-02 13:55:08 -07:00
parent ee46befd26
commit 0b1f0de7d2
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/inst_error.lean.expected.out
View file

@ -1,4 +1,4 @@
inst_error.lean:1:0: error: failed to synthesize type class instance for
inst_error.lean:1:38: error: failed to synthesize type class instance for
A : Type,
a b c : A
⊢ decidable (a = b ∧ a = c)