Hierarchical names

[jonsterling]

Lean has a really nice feature where names are hierarchical, so a single declaration foo might elaborate such that foo has a meaning, but also foo.x and foo.y etc. have meanings.