Explanation/documentation of `.{1}` notation?

Stream: new members

[Joe Glaberman]

Can someone please explain the meaning of the .{1} that appears in def test' : ℕ → ℕ := λ (n : ℕ), n + id_rhs.{1} ℕ 1? I am seeing this appear because I have set the options pp.generalized_field_notation=false and pp.universes=true

[Jason Rute]

docs#id_rhs has a universe parameter u. Whenever it is used, Lean must figure out what universe should fill that parameter. If you turn on that notion, then id_rhs.{u} makes that value explicit.

[Joe Glaberman]

That makes sense, thank you