unknown identifier

Stream: lean4

[Dean Young]

I have this example here:

def exams := Sigma (X : Prop), Sigma (y : Prop), Type

It gives

Main.lean:360:19: error: unknown identifier 'X'
Main.lean:360:28: error: expected command

[Henrik Böving]

Because you are using the sigma type via its identifier instead of its notation.

def exams := Σ (X : Prop), Σ (y : Prop), Type

[Dean Young]

Henrik Böving said:

Because you are using the sigma type via its identifier instead of its notation.

def exams := Σ (X : Prop), Σ (y : Prop), Type

Is there an ascii alternative?

[Dean Young]

Oh wait it's Sigma fun

[Henrik Böving]

Sigma fun X => Sigma fun y => Type

[Henrik Böving]

But I'd say if you are using Lean you won't be able to avoid unicode forever so you might as well embrace it :P

[Dean Young]

Hmm... thanks for the help and maybe so...

Oh and maybe you know how to get Type n as a function of n : Nat?

[Kevin Buzzard]

You can't do that because the n in Type n isn't a nat, it just looks like a nat.

[Dean Young]

Kevin Buzzard said:

You can't do that because the n in Type n isn't a nat, it just looks like a nat.

What about a predicate like "small" or "contained in Type n"

[Reid Barton]

You can say that there Exists an Equiv to a Type n -- even with only ASCII

[Reid Barton]

Henrik Böving said:

But I'd say if you are using Lean you won't be able to avoid unicode forever so you might as well embrace it :P

Yeah but you will have a lot more fun without unicode!

[Dean Young]

Reid Barton said:

Henrik Böving said:

But I'd say if you are using Lean you won't be able to avoid unicode forever so you might as well embrace it :P

Yeah but you will have a lot more fun without unicode!

Well, there was at least a point to it. I made this thing I call Mathematex, which is ultimately going to pack a bunch of things into a Latex package, maybe which calls my server of linearlibrary.org to perform the computing. Latex only works for ASCII as far as I can tell.