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 2022-10-06 07:41:48 -07:00
parent 87caf6d38a
commit 0577993d61
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -12,8 +12,8 @@ linterUnusedVariables.lean:51:11-51:12: warning: unused variable `z` [linter.unu
linterUnusedVariables.lean:56:14-56:15: warning: unused variable `y` [linter.unusedVariables]
linterUnusedVariables.lean:62:20-62:21: warning: unused variable `y` [linter.unusedVariables]
linterUnusedVariables.lean:67:34-67:38: warning: unused variable `inst` [linter.unusedVariables]
linterUnusedVariables.lean:109:6-109:7: warning: unused variable `y` [linter.unusedVariables]
linterUnusedVariables.lean:108:25-108:26: warning: unused variable `x` [linter.unusedVariables]
linterUnusedVariables.lean:109:6-109:7: warning: unused variable `y` [linter.unusedVariables]
linterUnusedVariables.lean:115:6-115:7: warning: unused variable `a` [linter.unusedVariables]
linterUnusedVariables.lean:125:26-125:27: warning: unused variable `z` [linter.unusedVariables]
linterUnusedVariables.lean:133:9-133:10: warning: unused variable `h` [linter.unusedVariables]

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

@ -19,7 +19,7 @@ inst✝ inst : α
shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder
context:
α : Type u_1
inst.71 : Inhabited α
inst.82 : Inhabited α
inst inst : α
⊢ {β δ : Type} → α → β → δ → α × β × δ
shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder