# Zulip Chat Archive

## Stream: general

### Topic: Problem with using "fun"

#### Kind Bubble (Nov 20 2022 at 23:31):

Maybe someone can help me here...

I was interested in getting all of my Lean 4 code to export to a purely ASCII format so I tried using "fun" instead of the usual lambda. I got this error:

`Main.lean:6:21: error: expected '=>'`

From the input:

`#check fun (X : Type), X`

#### Kevin Buzzard (Nov 20 2022 at 23:45):

That's because the lean 4 syntax isn't a comma, it's =>

#### Kind Bubble (Nov 21 2022 at 02:12):

Thanks.

Do you know ASCII equivalents of \Pi and \Sigma? What about \exists and \forall?

#### Julian Berman (Nov 21 2022 at 02:22):

I'm not sure there's any guarantee there'll always be one, certainly not for arbitrary notation, unless you're including writing out `Sigma.mk whatever`

.

`\exists`

and `\forall`

are `exists`

and `forall`

:

```
#check exists n, n ■ ∃ n, n : Prop
#check forall n, n ■ (n : Sort u_1) → n : Sort (imax (u_1 + 1) u_1)
```

I think `\Sigma`

doesn't have an ASCII equivalent, it's defined alongside `exists`

and probably would be near there: https://github.com/leanprover/lean4/blob/1b73fa3fa1f65fd0e857525866426ad6421b1e50/src/Init/NotationExtra.lean#L84-L85 but not sure.

#### Mario Carneiro (Nov 21 2022 at 02:34):

the ascii equivalent of \Sigma is `Sigma fun x : A => B x`

;)

#### Mario Carneiro (Nov 21 2022 at 02:36):

Also, you can use structure literals to do `Sigma.mk`

:

```
#check ({ fst := 0, snd := 2 } : Sigma fun _ : Nat => Nat)
```

#### Mario Carneiro (Nov 21 2022 at 02:37):

but the real answer here is that lean 4 has made no serious attempt to be ASCII compatible after years of strong support for unicode insertion from supported editors. There used to be more ascii-equivalent syntax that has been removed over the years, like `(|x, y|)`

for `⟨x, y⟩`

.

#### Mario Carneiro (Nov 21 2022 at 02:39):

writing lean in all ascii is similar to trying to write a javascript program that doesn't use the letter `e`

#### Kind Bubble (Nov 21 2022 at 03:13):

That's pretty funny.

Well, as long as I've come this far, I might as well ask if there's an analogue of Sigma fun for Pi. Maybe something like

`Pi (a: A,b : B(a) )`

#### Mario Carneiro (Nov 21 2022 at 03:18):

```
variable {A : Type} {B : A → Type}
example : (∀ x : A, B x) = ((x : A) → B x) := rfl
example : (Σ x : A, B x) = ((x : A) × B x) := rfl
```

#### Mario Carneiro (Nov 21 2022 at 03:19):

or, are you still asking about ascii equivalents?

```
variable {A : Type} {B : A → Type}
example : (∀ x : A, B x) = (forall x : A, B x) := rfl
example : (Σ x : A, B x) = (Sigma fun x : A => B x) := rfl
```

#### Mario Carneiro (Nov 21 2022 at 03:20):

yes, `forall`

works on types too

#### Mario Carneiro (Nov 21 2022 at 03:22):

you could define `Pi`

if you want it to look more similar to the other one though

```
def Pi {A} (B : A → Sort _) := forall x : A, B x
variable {A : Type} {B : A → Type}
example : (∀ x : A, B x) = (Pi fun x : A => B x) := rfl
example : (Σ x : A, B x) = (Sigma fun x : A => B x) := rfl
```

#### Mario Carneiro (Nov 21 2022 at 03:23):

(don't let the syntax highlighting mislead you here, `Pi`

isn't a keyword in lean 4 anymore, unlike lean 3)

#### Kind Bubble (Nov 21 2022 at 03:55):

Thanks Mario. You have a pretty thorough knowledge!

Last updated: Dec 20 2023 at 11:08 UTC