Example in lean

Stream: Is there code for X?

[Horatiu Cheval]

Could you please ask the question in a new thread (by specifying another topic when posting the message)? You posted it in a thread that's about something else

[Kevin Buzzard]

Did you mean to post in an old resolved stream? I'm not sure what the question is but Lean has example.

[Notification Bot]

This topic was moved here from #new members > Defining z.arg using modulus by Eric Wieser

[Vasu]

can we have named examples in Lean?

[Yakov Pechersky]

How does a named example differ from something named lemma?

[Floris van Doorn]

Examples cannot have names in Lean. Use def or lemma if you want to give it a name.