Lean 4 Library Documentation

Write clear, engaging documentation that teaches users how to understand and use Lean 4 libraries effectively.

Philosophy

Great library documentation is prosaic: it reads like well-written prose, not a reference manual. It tells a story—starting with the problem the library solves, building intuition through examples, and gradually revealing depth.

Principles:

1. Lead with the "why" — Before showing API, explain what problem this solves
2. Show, then tell — Code examples first, explanations second
3. Progressive disclosure — Simple cases first, advanced features later
4. Concrete over abstract — Real examples over type signatures
5. Assume intelligence, not knowledge — Readers are smart but may not know Lean idioms

Document Structure

README.md (Entry Point)

# Library Name

One sentence: what this library does and why you'd use it.

## The Problem

2-3 sentences describing the pain point this library addresses.
Use concrete scenarios the reader will recognize.

## Quick Example

```lean
-- Show the library solving the problem in 5-10 lines
-- This should be copy-pasteable and immediately useful

Installation

require libname from git "https://github.com/..." @ "v0.0.1"

Core Concepts

Brief overview of the mental model. What are the 2-3 key ideas a user needs to understand?

Getting Started

Walk through a realistic use case step-by-step.

Documentation

Link to detailed guides, API reference, examples.

License

MIT (or appropriate license)

### Guide Documents

For libraries with depth, create focused guides:

| Document | Purpose | Length |
|----------|---------|--------|
| `GUIDE.md` | Complete tutorial | 500-1500 lines |
| `CONCEPTS.md` | Mental model and theory | 200-500 lines |
| `COOKBOOK.md` | Problem → solution recipes | Variable |
| `MIGRATION.md` | Upgrading from older versions | As needed |
| `ARCHITECTURE.md` | How the library works internally | For contributors |

## Writing Patterns

### The Hook Opening

Start with recognition, not definition:

```markdown
❌ "Collimator is a profunctor optics library implementing van Laarhoven lenses."

✓ "Ever written code like this?

```lean
let user := { user with
  address := { user.address with
    city := "Boston"
  }
}

Collimator lets you write this instead:

let user := user |> address..city .~ "Boston"

"

### The Annotated Example

Show code, then explain it line by line:

```markdown
```lean
def fetchUser (id : UserId) : IO (Option User) := do
  let response ← client.get s!"/users/{id}"  -- ①
  let .ok body := response.status | return none  -- ②
  body.parse User  -- ③

Let's break this down:

1. Line 1: We make an HTTP GET request, interpolating the user ID into the path
2. Line 2: Pattern match on the response status—if it's not .ok, return none early
3. Line 3: Parse the response body into a User structure

### The Progression Pattern

Build complexity gradually:

```markdown
## Basic Usage

Start with the simplest case that does something useful:

```lean
let color := Color.red

Adding Customization

Now let's see how to create custom colors:

let color := Color.rgb 255 128 0

Advanced: Color Spaces

For precise color work, you can specify the color space:

let color := Color.hsl 0.0 1.0 0.5  -- Same red in HSL

### The "What You'll Build" Preview

For tutorials, show the end result upfront:

```markdown
## What We're Building

By the end of this guide, you'll have a working CLI that:
- Parses command-line arguments
- Reads configuration from a TOML file
- Makes HTTP requests to an API
- Displays results in a formatted table

Here's a preview of the final code:

```lean
def main (args : List String) : IO Unit := do
  let config ← Config.load "config.toml"
  let results ← Api.fetch config.endpoint
  Terminal.printTable results

Let's build this step by step.

### The Comparison Table

For choosing between options:

```markdown
## Choosing a Parser

| If you need... | Use... | Example |
|----------------|--------|---------|
| Simple key-value parsing | `basic` | Config files |
| Full grammar support | `grammar` | Programming languages |
| Streaming/incremental | `streaming` | Large files |
| Error recovery | `resilient` | IDE integration |

The Common Mistakes Section

Anticipate confusion:

## Common Mistakes

### Forgetting to import the instance

```lean
-- ❌ This won't compile
def x : Json := toJson myValue

-- ✓ Import the ToJson instance
import MyLib.Json
def x : Json := toJson myValue

Using pure instead of return in do-notation

Both work, but return short-circuits while pure continues:

-- These behave differently!
def f : IO Unit := do
  if condition then return  -- Exits immediately
  doMoreStuff

def g : IO Unit := do
  if condition then pure ()  -- Continues to doMoreStuff
  doMoreStuff

## Writing Style

### Voice and Tone

- **Active voice:** "The parser reads the file" not "The file is read by the parser"
- **Second person:** "You can configure..." not "One can configure..."
- **Present tense:** "This returns..." not "This will return..."
- **Direct:** "Use `map`" not "You might want to consider using `map`"

### Technical Precision

Be precise without being pedantic:

```markdown
❌ "This function takes a parameter and returns a value."
✓ "Given a user ID, returns the user's profile or `none` if not found."

❌ "The monad instance allows for sequential composition."
✓ "You can chain operations with `do` notation."

Code Comments

In documentation examples, comments explain the non-obvious:

-- ❌ Redundant comment
let x := 5  -- Set x to 5

-- ✓ Explains why, not what
let x := 5  -- Default timeout in seconds

-- ✓ Clarifies Lean-specific syntax
let (a, b) := pair  -- Destructure the tuple

Lean-Specific Documentation

Documenting Type Classes

## The `Parseable` Type Class

To make your type parseable from strings, implement `Parseable`:

```lean
class Parseable (α : Type) where
  parse : String → Option α

Required method:

• parse: Convert a string to your type, returning none on failure

Example implementation:

instance : Parseable MyConfig where
  parse s :=
    match s.splitOn "=" with
    | [key, value] => some { key, value }
    | _ => none

Automatic derivation:

For simple structures, use deriving Parseable (requires import Lib.Derive).

### Documenting Monads and Effects

```markdown
## The `Fetch` Monad

`Fetch` is a monad for making HTTP requests with automatic caching and retry.

```lean
def Fetch (α : Type) : Type := ReaderT FetchConfig (ExceptT FetchError IO) α

Running a Fetch action:

def main : IO Unit := do
  let config := FetchConfig.default
  match ← Fetch.run config myFetchAction with
  | .ok result => IO.println s!"Got: {result}"
  | .error e => IO.eprintln s!"Failed: {e}"

Available operations:

Operation	Type	Description
Fetch.get	String → Fetch Response	GET request
Fetch.post	String → Json → Fetch Response	POST with JSON body
Fetch.withTimeout	Nat → Fetch α → Fetch α	Set timeout (ms)

### Documenting Macros and DSLs

```markdown
## Query DSL

The `query` macro provides SQL-like syntax for building type-safe queries:

```lean
query {
  from users
  where age > 21
  select name, email
  orderBy name
  limit 10
}

Clauses:

Clause	Required	Description
from table	Yes	Source table
where condition	No	Filter rows
select fields	No	Choose columns (default: all)
orderBy field	No	Sort results
limit n	No	Maximum rows

The generated type:

The query macro produces a Query α where α is a structure containing the selected fields. The compiler infers this from your select clause.

### Documenting Notation

```markdown
## Custom Notation

This library defines several operators for working with lenses:

| Notation | Meaning | Example |
|----------|---------|---------|
| `a..b` | Compose lenses | `user..address..city` |
| `x ^. l` | View through lens | `user ^. name` |
| `l .~ v` | Set through lens | `name .~ "Alice"` |
| `l %~ f` | Modify through lens | `age %~ (· + 1)` |

**Precedence:** `..` binds tighter than `.~` and `%~`, so:

```lean
user |> address..city .~ "Boston"
-- Parses as: user |> ((address..city) .~ "Boston")

## API Reference Style

When documenting individual functions:

```markdown
### `Array.groupBy`

Groups elements by a key function, returning a map from keys to arrays of elements.

```lean
def groupBy [BEq κ] [Hashable κ] (f : α → κ) (xs : Array α) : HashMap κ (Array α)

Parameters:

• f: Function to extract the grouping key from each element
• xs: Array of elements to group

Returns: A HashMap where each key maps to all elements that produced that key

Example:

let words := #["apple", "banana", "apricot", "blueberry"]
let byFirstLetter := words.groupBy (·.front)
-- { 'a' => #["apple", "apricot"], 'b' => #["banana", "blueberry"] }

Performance: O(n) where n is the array length

See also: Array.partition, Array.filter

## Complete README Template

```markdown
# LibraryName

Brief, compelling description of what this library does.

## Why LibraryName?

Describe the problem space. What's hard without this library?
What does it make easy?

## Quick Start

```lean
import LibraryName

-- Minimal working example (10 lines or less)

Installation

Add to your lakefile.lean:

require libraryname from git "https://github.com/author/libraryname" @ "v1.0.0"

Features

• Feature One: Brief description
• Feature Two: Brief description
• Feature Three: Brief description

Examples

Common Use Case

-- Example with comments

Another Use Case

-- Example with comments

API Overview

Module	Purpose
LibraryName.Core	Essential types and functions
LibraryName.Utils	Helper utilities
LibraryName.Derive	Deriving instances

Documentation

• User Guide — Complete tutorial
• API Reference — Full API documentation
• Examples — Runnable example projects

Contributing

Contributions welcome! Please read CONTRIBUTING.md.

License

MIT License — see LICENSE

## Checklist

Before finalizing documentation:

- [ ] Can a new user understand what the library does in 30 seconds?
- [ ] Is there a copy-pasteable example in the first screenful?
- [ ] Are installation instructions complete and tested?
- [ ] Do examples actually compile and run?
- [ ] Are common mistakes addressed?
- [ ] Is the writing free of jargon (or is jargon explained)?
- [ ] Does progressive disclosure work (simple → complex)?
- [ ] Are type signatures accompanied by plain-English explanations?
- [ ] Is the tone consistent throughout?
- [ ] Are all code blocks syntax-highlighted correctly?