In coq mode I have ligatures being used: instead of "fun", it shows λ in the programming code. But in the comments lambda transformed into a character I can't even copy, so I'll attach a screenshot:


Something is wrong with the glyph. What font should I set to get lambda everywhere?

  • I had a look at coq-mode. It just uses font-lock-mode with syntactic highlighting and pretttify-symbols-mode. The face you are looking for should be font-lock-comment-face. Maybe, it is customized.
    – Tobias
    Sep 13, 2019 at 21:25
  • That looks more like a different character than a different font to me. You can check by putting your cursor on it and running C-u C-x = to show all the details about it. It'll tell you the name of the character as well as what font it used to draw it.
    – db48x
    Sep 14, 2019 at 3:57
  • @db48x It is the same character lambda.
    – user4035
    Sep 14, 2019 at 8:35
  • Sounds like the fonts used must be different.
    – db48x
    Sep 15, 2019 at 3:23
  • @db48x After using a different font - "Monoid", it started to work. But why is lambda correct in the code and incorrect in comments?
    – user4035
    Sep 20, 2019 at 19:37


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.