From d37d02b5124866e2c898432fb8d0bed2e5c4351d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Jan 2020 09:16:29 -0800 Subject: [PATCH] fix: more general instance --- src/Init/Control/Except.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 86dd59a674..6e5ad2c9c4 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -18,7 +18,7 @@ inductive Except (ε : Type u) (α : Type v) attribute [unbox] Except -instance {ε α : Type} [Inhabited ε] : Inhabited (Except ε α) := +instance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) := ⟨Except.error (arbitrary ε)⟩ section