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