Contents Previous Next

Naming conventions

• Naming conventions
  • Modules
  • Naming Conventions
  • Literate programming
  • Identifiers
  • Other material

Modules

In Lean, each file implicitly declares a module with the same name as the file (without the .lean extension). For example, a file named intro.lean implicitly declares a module named intro.

You can also explicitly declare modules within a file:

module MyModule where
  -- Module contents here

Modules can be imported using relative or absolute paths:

import Basic.Numbers            -- absolute import
import .Numbers                 -- relative import
import «Numbers»                -- import using Unicode characters

Naming Conventions

• Functions and Variables: Use snake_case (e.g., is_prime, find_max).
• Types and Structures: Use PascalCase (e.g., NaturalNumber, GroupTheory).
• Modules: Generally use PascalCase for module names, such as Data.List or Algebra.Ring.
• Constants and Axioms: Use descriptive names and often use PascalCase (e.g., ExcludedMiddle, AxiomOfChoice).

Literate programming

Lean supports literate programming through its .lean files. While not as extensive as Agda’s literate programming options, you can include markdown-style comments in your Lean files:

/-
# This is a markdown-style comment
It can span multiple lines and include *formatting*.
-/

def example := 42

Identifiers

Lean has some common naming practices, though they’re more guidelines than strict rules:

1. Functions and variables: Use snake_case (e.g., add_numbers, total_count)
2. Types and structures: Use PascalCase (e.g., NaturalNumber, BinaryTree)
3. Modules: Use PascalCase (e.g., Data.List, Logic.Propositional)
4. Constants and axioms: Often use PascalCase (e.g., Pi, ExcludedMiddle)
5. Unicode characters: Lean supports Unicode, so mathematical symbols are common (e.g., ∀, λ, →)
6. Notation: Lean has a powerful notation system for defining custom syntax

Remember that in Lean, clarity and readability are paramount. Choose names that accurately describe the purpose or behavior of the identifier. Consistency within a project or library is more important than strictly adhering to any particular convention.

Other material

Here’s a list of resources for learning Lean:

1. Lean’s official documentation: A great guide to get started with Lean 4.

2. Theorem Proving in Lean: An introduction to theorem proving using Lean.

3. Mathematics in Lean: A tutorial on formalizing mathematics in Lean.

4. Functional Programming in Lean: A guide to functional programming concepts in Lean.

5. Lean for the Curious Mathematician: An introduction to Lean for mathematicians.

6. Lean Zulip Chat: A community chat for Lean users and developers.

7. Lean Together: Materials from the Lean Together workshops.

8. Lean 4 Examples: A collection of example Lean 4 projects.

9. The Natural Number Game: An interactive tutorial for learning Lean through number theory.

10. Formal Abstractions: A YouTube channel with Lean tutorials and demonstrations.

Types