Code in backticks

GitHub, Zulip, and other Markdown-friendly sites support syntax highlighting for Lean.

When you post a snippet of Lean code that contains multiple lines, enclose it in triple backticks. On Zulip, this will automatically be highlighted as Lean code; on GitHub and other sites, use ```lean to open the code block.

For Zulip:

```
def my_nat : n := 5
#check my_nat
```

For GitHub:

```lean
def my_nat : n := 5
#check my_nat
```

This produces the pretty code block:

def my_nat : n := 5
#check my_nat

If you want to quote normal text on Zulip, you can use ```text or ```quote.

To post a snippet of code inline, enclose it in single backticks: `my code here`. If your code contains backticks itself, enclose it in more backticks than it contains: `` my`code`contains`backticks ``.

If you have already posted code without backticks, please edit your message to add them instead of posting again.