Advice on some characters not displaying in emacs on WSL

Stream: general

[Alex Zani]

I'm wondering if anyone might have advice on some characters not getting displayed correctly. (I assume) I'm using lean4-mode in emacs on WSL. I'm assuming I want new fonts or something?

image.png

[Eric Wieser]

Which characters are you assuming incorrect there?

[Floris van Doorn]

Maybe you were expecting to see the output of #check @List.map?

[Floris van Doorn]

The question marks are metavariables, they can (in this case) be instantiated for any type.

[Alex Zani]

I assumed the ?m.3 and ?m.4 were improperly displayed unicode characters. But it sounds like I was wrong?

[Yaël Dillies]

As Floris said, they stand for metavariables. Lean hasn't determined the type to put there. Giving it more information (with explicit type annotation, or by just using it for something) will make them go away.

[Kyle Miller]

Following Floris's suggestion, you get

#check @List.map
-- List.map : {α : Type u_1} → {β : Type u_2} → (α → β) → List α → List β

Without the @, Lean fills in all the implicit arguments (the ones indicated with curly braces) with metavariables. These are solved by the elaborator through unification. It's not a problem for #check, but well-typed programs need to have no metavariables.

def foo := List.map
/- output:
don't know how to synthesize implicit argument
  @List.map ?m.870 ?m.871
context:
⊢ Type u_2
tests.lean:18:11
don't know how to synthesize implicit argument
  @List.map ?m.870 ?m.871
context:
⊢ Type u_1
-/

[Alex Zani]

Thanks for clarification. :) In the spirit of just giving one datapoint, I first encountered that here: https://leanprover.github.io/lean4/doc/namespaces.html and I haven't read about metavariables yet, which is why I was confused. I expect that if the example had shown the expected output, I would not have been confused. But again, just one datapoint.

[Alex Zani]

Let me know if a PR adding the expected output to that page of the docs would be welcome. I have important things I'm procrastinating on. :-)

[Mario Carneiro]

Given that the book says it will discuss the types later, I think showing the output including a bunch of metavariables, or using #check @List.map with a weird unexplained sigil in the middle, would not flow very well in the context of the introduction

[Mario Carneiro]

I think the only relevant bit of information to take out of that test is that #check List.map succeeds while #check map fails

[Mario Carneiro]

perhaps #print List.map would be better to show this

[Alex Zani]

That's fair, but it already shows #check @List.cons in 4.5 earlier in the manual. I agree #print List.map might do a better job.

[Alex Zani]

Better job of demonstrating what open does without raising a bunch of other questions that is.