From b2181497fdee57705360d91fc6a89bcd030a4bba Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 16 Feb 2016 12:29:58 -0500 Subject: [PATCH] fix(tests): fix delta_issue2 --- tests/lean/hott/delta_issue2.hlean | 1 + 1 file changed, 1 insertion(+) 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)