From 856559a9835b691acd8ae1697766088b787e941d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Dec 2020 07:34:10 -0800 Subject: [PATCH] chore: fix test output --- tests/lean/pplevel.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/pplevel.lean.expected.out b/tests/lean/pplevel.lean.expected.out index cc9abba3ea..e6e05f6c2e 100644 --- a/tests/lean/pplevel.lean.expected.out +++ b/tests/lean/pplevel.lean.expected.out @@ -1,6 +1,6 @@ Type (max u v w) : Type ((max u v w) + 1) Type u : Type (u + 1) id.{max u v w} : {α : Sort (max u v w)} → α → α -Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max (w + 1) ((max u v) + 1)) +Monad.{max u v, w + 1} : (Type (max u v) → Type (w + 1)) → Type (max ((max u v) + 1) (w + 1)) Type (max (u + 1) w (v + 2)) : Type ((max (u + 1) w (v + 2)) + 1) Type u_1 : Type (u_1 + 1)