Zulip Chat Archive

Stream: general

Topic: Advice on some characters not displaying in emacs on WSL

Alex Zani (Aug 19 2021 at 16:27):

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?


Eric Wieser (Aug 19 2021 at 16:29):

Which characters are you assuming incorrect there?

Floris van Doorn (Aug 19 2021 at 16:32):

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

Floris van Doorn (Aug 19 2021 at 16:33):

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

Alex Zani (Aug 19 2021 at 16:50):

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

Yaël Dillies (Aug 19 2021 at 16:54):

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 (Aug 19 2021 at 16:57):

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
⊢ Type u_2
don't know how to synthesize implicit argument
  @List.map ?m.870 ?m.871
⊢ Type u_1

Alex Zani (Aug 19 2021 at 16:57):

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 (Aug 19 2021 at 17:01):

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 (Aug 19 2021 at 17:06):

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 (Aug 19 2021 at 17:07):

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 (Aug 19 2021 at 17:08):

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

Alex Zani (Aug 19 2021 at 17:09):

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 (Aug 19 2021 at 17:12):

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

Last updated: Dec 20 2023 at 11:08 UTC