# Zulip Chat Archive

## Stream: lean4

### Topic: fun with syntax ambiguity

#### Mario Carneiro (Feb 01 2021 at 21:48):

I don't know if we can/should do anything about this, but it's amusing to me to see how type ascription, implication and the new "dependent implication" syntax interact:

```
#check Nat → Prop -- Nat → Prop : Type
#check (Nat : Type) → Prop -- Type → Prop : Type 1
#check (Int : Type) → Prop -- Type → Prop : Type 1
#check (Prop : Type) → Prop -- Prop → Prop : Type
#check ((Nat : Type)) → Prop -- Nat → Prop : Type
```

#### Sebastian Ullrich (Feb 01 2021 at 21:50):

Looks perfectly reasonable to me :big_smile:

#### Mario Carneiro (Feb 01 2021 at 21:52):

also:

```
#check (id Nat : Type) → Prop -- Type → Type → Prop : Type 1
#check ((id Nat) : Type) → Prop -- id Nat → Prop : Type
```

#### Leonardo de Moura (Feb 01 2021 at 22:39):

@Mario Carneiro I don't see any surprises above. Note that `Prop`

is not an identifier, but a keyword.

Disclaimer: the "dependent implication" notation is off-limits, I love it and we use it all the time :)

We could try to change the type ascription notation. David Christiansen told me they use `the <type> <expr>`

in Idris, where `the`

is just our `id`

where the type is an explicit argument. I think Agda uses `<type> ∋ <expr>`

, but this is probably not a good match for mathlib :)

#### Mario Carneiro (Feb 01 2021 at 23:28):

I think I'll get along just fine with the new notation; with the lack of initial symbol it's a little bit of a garden path notation but I don't think it's too big of a deal. I don't know whether we should learn to love this notation or find a way to change it to `∀`

for actual for-all statements in mathematics like `∀ x : Nat, ∃ p : Prime, p > x`

though.

#### Mario Carneiro (Feb 01 2021 at 23:31):

currently that pretty prints as `(x : Nat) → Exists fun (p : Prime) => p > x : Prop`

btw, so I'm sure we'll be adding delaborator extensions in the mathlib prelude for this

#### Leonardo de Moura (Feb 01 2021 at 23:52):

We can add a flag for pretty-printing "dependent implication" using `∀`

.

The delaborator for `Exists`

and `Subtype`

are missing right now, but they will be added soon.

#### Mario Carneiro (Feb 01 2021 at 23:55):

In lean 3, there was an automatic switch between `\forall`

and `\Pi`

depending on the universe. Would something like that be acceptable here, where the prop version is `\forall (x : A), B x`

and the type version is `(x : A) -> B x`

?

#### Leonardo de Moura (Feb 02 2021 at 00:08):

Mario Carneiro: In lean 3, there was an automatic switch between \forall and \Pi depending on the universe. Would something like that be acceptable here, where the prop version is \forall (x : A), B x and the type version is (x : A) -> B x?

Yes, this is reasonable.

#### Eric Wieser (Feb 02 2021 at 00:15):

The docs claim the old sigma notation is still legal

#### Mario Carneiro (Feb 02 2021 at 00:16):

the example `∀ x : Nat, ∃ p : Prime, p > x`

parses in lean 4 today, so it looks like that has not changed

#### Mario Carneiro (Feb 02 2021 at 00:16):

it's just the pretty printing that is not supported yet

#### Mario Carneiro (Feb 02 2021 at 00:18):

However `Sigma`

's notation has also changed, to `(x : A) × B x`

(which makes good sense to me)

#### Mario Carneiro (Feb 02 2021 at 00:22):

`PSigma`

, `Subtype`

and `Exists`

all have no pretty printing notation, but `{x // p x}`

and ` ∃ x, p x`

work as parser input. (`PSigma`

doesn't have any parser notation, although I'm not particularly fussed about losing `Σ'`

. We could do `(x : A) ×' B x`

if we want something similar)

#### Nasos Evangelou-Oost (Feb 02 2021 at 04:21):

is mathlib compatible with lean4?

#### Huỳnh Trần Khanh (Feb 02 2021 at 04:23):

Not yet but it will eventually. Also this is offtopic for this thread. Create a new one.

#### Huỳnh Trần Khanh (Feb 02 2021 at 04:23):

@Nasos Evangelou-Oost tag to get your attention

#### Eric Wieser (Feb 02 2021 at 10:38):

Eric Wieser said:

Only tangentially related to this thread, but if commas are no longer used to introduce binders in functions, is the intent to also avoid them in unions/sums/existential notation, all of which are syntactic sugar for a function?

Taking docs#tsum as an example, it seems odd to require `=>`

in `tsum $ λ i => f i`

yet use a comma in `∑' i, f i`

(c.f. lean 3's `tsum $ λ i, f i`

, where `∑'`

can be read as a shorthand for `tsum $ λ`

). We could make these consistent by making the lean4 notation for `tsum`

`∑' i => f i`

, but I suspect that would be unpopular.

Last updated: May 07 2021 at 12:15 UTC