From 498d7886eb8563ec35818c02235fd9e2b20d3db4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Sep 2020 13:21:58 -0700 Subject: [PATCH] chore: fix test output --- tests/lean/emptyc.lean.expected.out | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/lean/emptyc.lean.expected.out b/tests/lean/emptyc.lean.expected.out index c4bbb21125..bf04222f96 100644 --- a/tests/lean/emptyc.lean.expected.out +++ b/tests/lean/emptyc.lean.expected.out @@ -1 +1,4 @@ -emptyc.lean:19:0: error: ambiguous, possible interpretations [{x := 0}, ∅] +emptyc.lean:19:0: error: ambiguous, possible interpretations + {x := 0} + + ∅