Problem with using "fun"

Stream: general

[Kind Bubble]

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]

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

[Kind Bubble]

Thanks.

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

[Julian Berman]

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]

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

[Mario Carneiro]

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

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

[Mario Carneiro]

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]

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

[Kind Bubble]

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]

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]

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]

yes, forall works on types too

[Mario Carneiro]

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]

(don't let the syntax highlighting mislead you here, Pi isn't a keyword in lean 4 anymore, unlike lean 3)

[Kind Bubble]

Thanks Mario. You have a pretty thorough knowledge!