From b1faed895acd89184aad4383489b043fa6236d14 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Feb 2021 08:36:03 -0800 Subject: [PATCH] chore: change `inferInstance` and `inferInstanceAs` types --- src/Init/Prelude.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index ceb94899cc..8a93546630 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -18,8 +18,8 @@ abbrev Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) ( abbrev Function.const {α : Sort u} (β : Sort v) (a : α) : β → α := fun x => a -@[reducible] def inferInstance {α : Type u} [i : α] : α := i -@[reducible] def inferInstanceAs (α : Type u) [i : α] : α := i +@[reducible] def inferInstance {α : Sort u} [i : α] : α := i +@[reducible] def inferInstanceAs (α : Sort u) [i : α] : α := i set_option bootstrap.inductiveCheckResultingUniverse false in inductive PUnit : Sort u where