From 382928f0fafeb2f9c266457c8375f7cdc4359906 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Sep 2016 10:05:55 -0700 Subject: [PATCH] fix(library/init/logic): typo --- library/init/logic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/logic.lean b/library/init/logic.lean index fca104650b..123908a9c1 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -787,7 +787,7 @@ protected definition inhabited.value {A : Type u} : inhabited A → A := λ h, inhabited.rec (λ a, a) h attribute [inline] -protected definition inhabited.destruct {A : Type u} {B : Type u} (H1 : inhabited A) (H2 : A → B) : B := +protected definition inhabited.destruct {A : Type u} {B : Type v} (H1 : inhabited A) (H2 : A → B) : B := inhabited.rec H2 H1 attribute [inline]