From 8f6444c76af08e9c0023ec70eef0b90dd64fca39 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 16 Mar 2019 18:42:37 -0700
Subject: [PATCH] chore(library/init/core): remove todo

---
 library/init/core.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/library/init/core.lean b/library/init/core.lean
index 80831246fc..56f8b0d924 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -1395,8 +1395,7 @@ end plift
 class inhabited (α : Sort u) :=
 (default : α)
 
--- TODO: mark as opaque
-def default (α : Sort u) [inhabited α] : α :=
+constant default (α : Sort u) [inhabited α] : α :=
 inhabited.default α
 
 @[inline, irreducible] def arbitrary (α : Sort u) [inhabited α] : α :=