method ident space sensitivity

Stream: new members

[Xiyu Zhai]

I do not understand the following

-- incorrect
-- errors
-- type mismatch
--   List.all as
-- has type
--   (Nat → Bool) → Bool : Type
-- but is expected to have type
--   Bool : TypeLean 4
def method_without_space(as: List Nat): Bool :=
  as.all(fun a => true)

-- correct
def method_with_space(as: List Nat): Bool :=
  as.all (fun a => true)

[Xiyu Zhai]

Why a space is needed after as.all

[Simon Daniel]

to apply a function you write the function name and then the arguments seperated by spaces

[Xiyu Zhai]

I see

[Xiyu Zhai]

So if not spaced, what will the compiler see it as? Maybe this is not an interesting question

[Simon Daniel]

i found this book very useful as a referenceFunctional Programming Book

[Simon Daniel]

Xiyu Zhai said:

So if not spaced, what will the compiler see it as? Maybe this is not an interesting question

I also get the message: unexpected token '('; expected command, so i guess its simply not valid to omit the space

[Xiyu Zhai]

Oh, I didn't notice that
It seems that type error and syntax error get mixed up and I only saw the type error.

[Xiyu Zhai]

type mismatch
  List.all allocations
has type
  (BareMetalMemoryAllocation → Bool) → Bool : Type
but is expected to have type
  Prop : TypeLean 4
unexpected token '('; expected commandLean 4

[Xiyu Zhai]

I would suggest it's better to have a original/derived error system. Only show those errors that are original.

[Xiyu Zhai]

In CPP, the error system is notorious because it's too hard to find the original one.

[Simon Daniel]

seeing only the type error would be indeed confusing
if youre using VSCode the Lean Info view shows 2 seperate messages in this case

[Xiyu Zhai]

Indeed I’m using Vscode

[Xiyu Zhai]

But I only see the type error if I’m not hovering my mouse over the ‘(‘

[Simon Daniel]

btw i think it just ignores the part after '(' for the type error, since "as.all" has type (Nat → Bool) → Bool