From 89d0f1773e9fb60688ede61b0bb0e8dfd07e8668 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 11 Mar 2017 18:41:37 -0800 Subject: [PATCH] chore(tests/lean/inductive_resultant_level_inferrence): update expected output --- .../lean/inductive_resultant_level_inference.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/inductive_resultant_level_inference.lean.expected.out b/tests/lean/inductive_resultant_level_inference.lean.expected.out index 4f87d491fe..da529e94c5 100644 --- a/tests/lean/inductive_resultant_level_inference.lean.expected.out +++ b/tests/lean/inductive_resultant_level_inference.lean.expected.out @@ -18,7 +18,7 @@ X5.foo.{u} : Sort u → Sort (max 1 u) X6.foo.{u} : Sort u → Type (u+2) 7. ?U unifies with a max: error -inductive_resultant_level_inference.lean:82:0: error: resultant level unifies with complex level 'max u_2 u_1', provide the universe levels explicitly +inductive_resultant_level_inference.lean:82:0: error: resultant level unifies with complex level 'max u_1 u_2', provide the universe levels explicitly 8. wrapping inductive returns element in different universe: error inductive_resultant_level_inference.lean:92:0: error: nested occurrence 'X8.bar.{(max 1 v)} foo' lives in universe 'succ (max 1 v)' but must live in resultant universe 'max 1 v'