Expected token

Stream: lean4

[Dean Young]

import Init.Data.ToString.Basic

does anyone know why the second line here gives "expected token"?

def Cat :=
Σ(Obj:Type 1),
Σ(Mor:Π(_:Obj),Π(_:Obj),(Type 1)),
Σ(Id:Π(X:Obj),Mor X X),
Σ(Mul:Π(X:Obj),Π(Y:Obj),Π(Z:Obj),Π(_:Mor X Y),Π(_:Mor Y Z),(Mor X Z)),
Σ(_:Π(X:Obj),Π(Y:Obj),Π(f:Mor X Y),Π(_:(Mul X Y Y) f (Id Y) = f),Unit),
Σ(_:Π(X:Obj),Π(Y:Obj),Π(f:Mor X Y),Π(_:(Mul X X Y) (Id X) f = f),Unit),
Σ(_:Π(X:Obj),Π(Y:Obj),Π(f:Mor X Y),Π(_:(Mul X X Y) (Id X) f = f),Unit),
Unit
def main := IO.println ""

[Arthur Paulino]

What's the type of Cat?

[Reid Barton]

You can't write pi types with a Π in Lean 4.

[Dean Young]

Reid Barton said:

You can't write pi types with a Π in Lean 4.

What is the correct way?

or if there isn't one how could I make notation like

notation Π => forall

[Arthur Paulino]

Is Cat a List? An Array? Prod?
I think that's a syntax error. You can't separate elements like that by just using comma and a linebreak

[Dean Young]

Arthur Paulino said:

Is Cat a List? An Array? Prod?
I think that's a syntax error. You can't separate elements like that by just using comma and a linebreak

I think it's Type 2

[Arthur Paulino]

Oh, wait, now I understood what you're trying to do

[Dean Young]

Arthur Paulino said:

Oh, wait, now I understood what you're trying to do

What do you think? Probably most people would have used structure, but I'm a bit of a purist :)

[Arthur Paulino]

I'm not sure. That's not the type of work that I usually do with Lean 4

[Reid Barton]

You can use ∀ instead, or the Agda-style (a : A) -> B a.

[Reid Barton]

Also, you can use spaces.