From 0577993d61360edf80189500912919cd0a1479d4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Oct 2022 07:41:48 -0700 Subject: [PATCH] chore: fix tests --- tests/lean/linterUnusedVariables.lean.expected.out | 2 +- tests/lean/shadow.lean.expected.out | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out index 0f69453305..2391423ea9 100644 --- a/tests/lean/linterUnusedVariables.lean.expected.out +++ b/tests/lean/linterUnusedVariables.lean.expected.out @@ -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] diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out index b75cd4a6e3..f98bfc46c2 100644 --- a/tests/lean/shadow.lean.expected.out +++ b/tests/lean/shadow.lean.expected.out @@ -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