Help with guillemet symbol

Stream: lean4

[Alex Sweeney]

image.png

The small guillemet symbols on line 1 were included with my initial project. How do I type them? I don't see it mentioned in Functional Programming with Lean or the Lean 4 book.

[Kevin Buzzard]

Hover over any symbol in VS Code to find out how to type it

[Alex Sweeney]

Thank you!

[Marc Huisinga]

A less known feature of the VS Code extension is also that you can display the full list of abbreviations by using Ctrl+Shift+P > Lean 4: Show all abbreviations

[Alex Sweeney]

Is anyone aware of these tips being documented somewhere and I just missed it? I spent probably 15 minutes trying to figure it out before asking here, and I imagine some new users might just get frustrated and give up if they can't figure out this one thing super early in the learning process.

[Alex Sweeney]

And this is coming from a software engineer, I work with VS Code almost daily and I just didn't think to hover over the symbol.

[Patrick Massot]

I know it appears very early in Mathematics in Lean.

[Patrick Massot]

I don't know about #fpil (@David Thrane Christiansen?) that you probably prefer to read first if you come from software engineering.

[Alex Sweeney]

Yep, I had not seen Mathematics in Lean yet.

[David Thrane Christiansen]

It's described in the introduction in FPiL, but I suspect that many readers skip over that. I'll make an issue in the repo to add some back-references the first few times non-ASCII Unicode occurs in code samples.

[David Thrane Christiansen]

Issue here: https://github.com/leanprover/fp-lean/issues/127

Thank you for the feedback! I'll have time to work on the book next month.