max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/core): remove todo

Browse source
This commit is contained in:
Leonardo de Moura 2019-03-16 18:42:37 -07:00
parent 1935986f3c
commit 8f6444c76a
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/core.lean
View file

@ -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 α] : α :=