In Lean 4: Comment lines #13

Hello everyone,

In this post, I will talk about how to use comment lines in Lean 4 and explain what this concept means for those who are hearing it for the very first time.

First of all, to create a comment line in Lean, we place two hyphens side by side: --. Anything we write after this will be considered a comment line, even if it is actually Lean code.

So, what is a comment line?

In short, it is a line that is ignored when running the code.

What is it used for?

It allows you to take notes, write entire paragraphs, or disable a line while testing code by simply adding -- to the front instead of deleting it completely. The rest is actually up to your creativity.

With that in mind, since I use the code editor as my own workspace while studying Lean 4, I add the Turkish translation of the book directly into it — as comments, of course.

Initially, this was a bit challenging for me because the font and color remained exactly the same throughout the file. Later on, I learned about certain features used within comment lines that allow you to do things like changing the color and modifying the font style.

I would also like to talk about those features in this post…

First of all, let me draw your attention once again to the fact that these are used within areas that have already been turned into comment lines.

Here are two things I discovered for changing colors:

--**the color has changed**

The key detail you need to pay attention to here is that there should be no whitespaces where the symbols meet the text on either side!

The other one:

--the color has changed``

The "no whitespaces" rule applies here as well!

--*italic*

Available in this link: https://github.com/fizikzedenin-kodlari/LeanOnMath/blob/main/commentLine%2313.lean

WhatsApp channel link to get instant updates on new posts: https://whatsapp.com/channel/0029VbDJCPQ4NVinQrRkA11O

Stay with coding!