From ea87dd48e3c60172bfdfcda04ecabff72e7fded3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 May 2015 18:18:57 -0700 Subject: [PATCH] chore(tests/lean/hott/inj_tac): fix typo --- tests/lean/hott/inj_tac.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/hott/inj_tac.hlean b/tests/lean/hott/inj_tac.hlean index 622bb11238..1b8be6c595 100644 --- a/tests/lean/hott/inj_tac.hlean +++ b/tests/lean/hott/inj_tac.hlean @@ -11,7 +11,7 @@ end example (A : Type) (n : nat) (v w : vector A n) (a : A) (b : A) : a :: v = b :: w → b = a := begin - intro H, injection H with aeqb beqw, + intro H, injection H with aeqb neqn beqw, rewrite aeqb end