Zulip Chat Archive

Stream: new members

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

Joe Glaberman (Aug 18 2022 at 00:05):

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 (Aug 18 2022 at 00:23):

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 (Aug 18 2022 at 00:32):

That makes sense, thank you

Last updated: Dec 20 2023 at 11:08 UTC