diff --git a/tests/lean/hott/delta_issue2.hlean b/tests/lean/hott/delta_issue2.hlean
index 47b6fbe4b5..e4f55d1059 100644
--- a/tests/lean/hott/delta_issue2.hlean
+++ b/tests/lean/hott/delta_issue2.hlean
@@ -1,4 +1,5 @@
 open nat eq
+infixr + := sum
 
 theorem add_assoc₁ : Π (a b c : ℕ), (a + b) + c = a + (b + c)
 | a b 0 := eq.refl (nat.rec a (λ x, succ) b)