Adding inline Lean Code🔗

You can include Lean code that is elaborated directly within the document. This is useful for small snippets. Please note that your lean code should follow the Lean syntax conventions of naming, casing variables, etc.