Sigma and Pi types

Stream: lean4

[James Caldwell]

Is there a library I can load to be able to use the standard notations for dependent types?

$\Sigma x:\tau, p x\;\;\;$ and $\;\;\; \Pi x:\tau, p x$

I get the symbols, $\Pi$ and $\Sigma$ but they don't seem to be bound to the corresponding dependent types.

[Martin Dvořák]

Unfortunately, the notation seems to have disappeared from Lean:
https://github.com/leanprover/lean4/blob/master/doc/lean3changes.md#dependent-function-types

[Henrik Böving]

Only the Pi one, it was replaced in favour of (x : t) -> p x or the forall one. Sigma you can still use

[James Caldwell]

OK - I see that $\forall x:\tau,p x$ is equivalent - I can live with that. Looking at Core.lean, it seems like someome could roll their own which is why I asked.

[Patrick Massot]

You can definitely define your own notation.

[Eric Wieser]

Lean 3 had Σ i : ι, p i and Π i : ι, p i. Lean4 encourages you to write those as (i : ι) × p i and (i : ι) → p i, although for whatever reason only actually removed the pi syntax and left the sigma syntax intact.