@kha note that the previous commit produced a small code bloat here.
The code bloat seems reasonable and affects definitions such as:
```
@[inline] protected def max : rbmap α β lt → option (α × β)
| ⟨t, _⟩ :=
match t.max with
| some ⟨k, v⟩ := some (k, v)
| none := none
```
Before previous commit, while compiling `max` we would not know it is
marked as `[inline]`. Thus, we would not inline `max._main` into
`max`. Now, we do.
I believe this is not a big deal since functions marked as `[inline]`
are supposed to be small.
