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

chore(library/init/control/id): spurious [inline] annotations

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-05 11:54:33 -07:00
parent c44f79f981
commit e7f379fb0f
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/control/id.lean
View file

@ -20,11 +20,11 @@ f x
@[inline] def Id.map {α β : Type u} (f : α → β) (x : Id α) : Id β :=
f x
@[inline] instance : Monad Id :=
instance : Monad Id :=
{ pure := @Id.pure, bind := @Id.bind, map := @Id.map }
@[inline] def Id.run {α : Type u} (x : Id α) : α :=
x
@[inline] instance : MonadRun id Id :=
instance : MonadRun id Id :=
⟨@Id.run⟩