Inferred namespace syntax

Stream: lean4

[Mario Carneiro]

Just posting here for visibility: Lean 4 just got "co-" projection/dot notation (lean4#944). You can use the syntax .foo (this is distinct from regular projection because it has a required space or non-expression before it, like f .foo or (.foo x)) to call a function foo in a namespace inferred from the result type. This is in particular useful for inductive types:

example (h : p) : p ∨ q := .inl h

I will certainly be using this a lot in the future. Way to go Lean 4 team!