### Expr.app Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Example JSON for creating 'Nat applied_to bvar_0'.

```json
{"ie": 0, "const": {"name": 1, "us": []}}
{"ie": 1, "bvar": 0}
{"ie": 2, "app": {"fn": 0, "arg": 1}}
```

--------------------------------

### Level.param Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

This example demonstrates how to represent a universe parameter, such as '?u', by referencing a name index.

```json
{"in": 1, "str": {"pre": 0, "str": "u"}}
```

```json
{"il": 1, "param": 1}
```

--------------------------------

### Expr.lam Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Example JSON for creating 'fun (x : Nat) => x'. The 'binderInfo' is set to 'default'.

```json
{"ie": 0, "const": {"name": 1, "us": []}}
{"ie": 1, "bvar": 0}
{"in": 2, "str": {"pre": 0, "str": "x"}}
{"ie": 2, "lam": {"name": 2, "type": 0, "body": 1, "binderInfo": "default"}}
```

--------------------------------

### Level.imax Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

This example shows the creation of a level using the implicative maximum function.

```json
{"il": 1, "imax": [0, 2]}
```

--------------------------------

### Example: Exporting Mathlib

Source: https://github.com/leanprover/lean4export/blob/master/README.md

This example demonstrates how to export the top-level `Mathlib` module from the `mathlib4` directory. The output is redirected to `out.ndjson`.

```sh
lake env ../.lake/build/bin/lean4export Mathlib > out.ndjson
```

--------------------------------

### Expr.const Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Example JSON for creating 'Nat' (a constant with no universe parameters).

```json
{"in": 1, "str": {"pre": 0, "str": "Nat"}}
{"ie": 0, "const": {"name": 1, "us": []}}
```

--------------------------------

### Complete Usage Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-parse-module.md

Demonstrates how to open an export file, read its content, parse it into an `ExportedEnv`, and access the parsed constants and their order. This example covers file I/O and data access after parsing.

```Lean
-- Open and read export file
let handle ← IO.FS.Handle.mk "output.ndjson" IO.FS.Mode.read
let stream ← handle.readToEnd

-- Parse into ExportedEnv
let env ← parseStream stream
handle.close

-- Access parsed constants
env.constMap.forM fun (name, info) => do
  IO.println s!"Constant: {name}"
  match info with
  | .axiomInfo ax => IO.println s!"  Type: {ax.type}"
  | .defnInfo def => IO.println s!"  Value: {def.value}"
  | _ => ()

-- Iterate in export order
env.constOrder.forM fun name =>
  IO.println s!"Exported: {name}"
```

--------------------------------

### Expr.letE Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Example JSON for creating 'let x : Nat := zero; x'. 'nondep' is set to false.

```json
{"ie": 0, "const": {"name": 1, "us": []}}
{"ie": 1, "const": {"name": 2, "us": []}}
{"ie": 2, "bvar": 0}
{"in": 3, "str": {"pre": 0, "str": "x"}}
{"ie": 3, "letE": {"name": 3, "type": 0, "value": 1, "body": 2, "nondep": false}}
```

--------------------------------

### Expr.strVal Examples

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Examples of string literals, including a non-empty string and an empty string.

```json
{"ie": 0, "strVal": "hello"}
{"ie": 1, "strVal": ""}
```

--------------------------------

### Expr.proj Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Example JSON for creating 'bvar_0.2', representing the second projection of a Prod structure.

```json
{"in": 1, "str": {"pre": 0, "str": "Prod"}}
{"ie": 0, "bvar": 0}
{"ie": 1, "proj": {"typeName": 1, "idx": 1, "struct": 0}}
```

--------------------------------

### Name.num Component Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

This example shows the creation of a name with a numeric component relative to an anonymous prefix.

```json
{"in": 1, "num": {"pre": 0, "i": 42}}
```

--------------------------------

### Example Axiom JSON

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

A concrete example of an axiom's JSON representation.

```json
{"axiom": {"name": 1, "levelParams": [], "type": 0, "isUnsafe": false}}
```

--------------------------------

### Expr.forallE Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Example JSON for creating '∀ (x : Nat), Nat'. The binder 'x' is associated with index 2.

```json
{"ie": 0, "const": {"name": 1, "us": []}}
{"in": 2, "str": {"pre": 0, "str": "x"}}
{"ie": 1, "const": {"name": 3, "us": []}}
{"ie": 2, "forallE": {"name": 2, "type": 0, "body": 1, "binderInfo": "default"}}
```

--------------------------------

### Definition with Dependencies Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Example of a JSON export for a definition with dependencies. It shows how names and types are referenced using indices.

```json
{"in":1,"str":{"pre":0,"str":"Nat"}}
{"in":2,"str":{"pre":1,"str":"zero"}}
{"in":3,"str":{"pre":1,"str":"succ"}}
{"const":{"name":1,"us":[]},"ie":0}
{"const":{"name":2,"us":[]},"ie":1}
{"const":{"name":1,"us":[]},"ie":2}
{"const":{"name":3,"us":[]},"ie":3}
{"app":{"fn":3,"arg":2},"ie":4}
{"def":{"name":4,"levelParams":[],"type":0,"value":4,"hints":"safe","safety":"safe","all":[4]}}
```

--------------------------------

### Level.max Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

This example demonstrates the creation of a level using the maximum of two other levels, resulting in succ(zero).

```json
{"il": 1, "succ": 0}
```

```json
{"il": 2, "max": [0, 1]}
```

--------------------------------

### Import Modules for Environment Setup

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Imports specified modules to build the Lean environment, ensuring all transitive dependencies are loaded and elaborated.

```lean
let imports := imports.toArray.map fun mod => { module := Syntax.decodeNameLit ("`" ++ mod) |>.get! }
let env ← importModules imports {}
```

--------------------------------

### Name.str Component Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

These examples demonstrate how to create names with string components. Index 0 is anonymous, index 1 is 'Nat' relative to anonymous, and index 2 is 'zero' relative to 'Nat'.

```json
{"in": 0, "str": {"pre": 0, "str": "Nat"}}
```

```json
{"in": 1, "str": {"pre": 0, "str": "zero"}}
```

--------------------------------

### Expr.sort Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Example JSON for creating Type 1 (type at level succ(zero)).

```json
{"il": 1, "succ": 0}
{"ie": 0, "sort": 1}
```

--------------------------------

### parseStream Example Usage

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-parse-module.md

Example demonstrating how to use `parseStream` to parse an export file and access the resulting constants.

```Lean
let h ← IO.FS.Handle.mk "export.ndjson" IO.FS.Mode.read
let stream ← h.readToEnd
let result ← parseStream stream
-- result.constMap contains all parsed constants
-- result.constOrder preserves export order
```

--------------------------------

### Metadata Object Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

An example of the metadata object as it would appear in an NDJSON export file.

```json
{"meta":{"exporter":{"name":"lean4export","version":"3.1.0"},"lean":{"version":"v4.30.0-rc2","githash":"<hash>"},"format":{"version":"3.1.0"}}}
```

--------------------------------

### Duplicate Axiom Declaration Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/errors.md

This example demonstrates a duplicate axiom declaration error. Ensure each constant name appears only once in the export file.

```json
{"axiom":{"name":1,"levelParams":[],"type":2,"isUnsafe":false}}
{"axiom":{"name":1,"levelParams":[],"type":3,"isUnsafe":false}}  # Error: Duplicate
```

--------------------------------

### Sample Declaration Format

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Example of a 'declaration' item in the NDJSON export format, showing an axiom with its properties.

```json
{"axiom":{"name":1,"levelParams":[],"type":0,"isUnsafe":false}}
```

--------------------------------

### Minimal Export Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

A minimal JSON export of a module containing a single axiom. Shows the structure of metadata and a simple axiom declaration.

```json
{"meta":{"exporter":{"name":"lean4export","version":"3.1.0"},"lean":{"version":"v4.30.0","githash":"abc123"},"format":{"version":"3.1.0"}}}
{"in":1,"str":{"pre":0,"str":"Nat"}}
{"il":1,"succ":0}
{"ie":0,"sort":1}
{"axiom":{"name":1,"levelParams":[],"type":0,"isUnsafe":false}}
```

--------------------------------

### Parse Command-Line Arguments

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Partitions command-line arguments into options, modules, and constants. Options start with '--' and have a minimum length of 3.

```lean
let (opts, args) := args.partition (fun s => s.startsWith "--" && s.length ≥ 3)
let (imports, constants) := args.span (· != "--")
```

--------------------------------

### Name.str Format Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/errors.md

This illustrates the expected JSON format for Name.str. It requires 'pre' and 'str' fields.

```json
{
  "pre": <number>,
  "str": "<string>"
}
```

--------------------------------

### JSON Format Examples for Name Serialization

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Provides examples of the JSON format used for serializing Lean names, including anonymous names, `Name.str`, and `Name.num`.

```json
{"in": 0}                              // anonymous
{"str": {"pre": 0, "str": "foo"}, "in": 1}  // Name.str
{"num": {"pre": 1, "i": 5}, "in": 2}       // Name.num
```

--------------------------------

### Expr.natVal Examples

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Examples of natural number literals, including a standard value and a large arbitrary precision number.

```json
{"ie": 0, "natVal": "42"}
{"ie": 1, "natVal": "99999999999999999999"}
```

--------------------------------

### Name.num Format Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/errors.md

This illustrates the expected JSON format for Name.num. It requires 'pre' and 'i' fields.

```json
{
  "pre": <number>,
  "i": <number>
}
```

--------------------------------

### Missing Constant Panic Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/errors.md

This bash command demonstrates how a missing constant in the environment triggers a panic during export. Ensure constant names are spelled correctly and exist in the environment.

```bash
lake env ../build/bin/lean4export Mathlib -- NonExistent
# Panic: Constant `NonExistent` not found in environment.
```

--------------------------------

### JSON Format Examples for Level Serialization

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Illustrates the JSON format for serializing Lean universe levels, covering `Level.succ`, `Level.max`, `Level.imax`, and `Level.param`.

```json
{"il": 1, "succ": 0}                    // Level.succ
{"il": 2, "max": [1, 0]}                // Level.max
{"il": 3, "imax": [1, 0]}               // Level.imax
{"il": 4, "param": 1}                   // Level.param
```

--------------------------------

### Name Index Not Found Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/errors.md

This JSON example illustrates a forward reference error in a Lean export file, where a name index is referenced before it is defined. This indicates a malformed export file or corrupted index map.

```json
# Forward reference to name index 5 before it's defined
{"ie":0,"const":{"name":5,"us":[]}}  # Error: Name not found 5
{"in":5,"str":{"pre":0,"str":"Nat"}}  # Name 5 defined here
```

--------------------------------

### Level.succ Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

This JSON object represents the successor of a level, effectively creating level 1 (succ(zero)).

```json
{"il": 1, "succ": 0}
```

--------------------------------

### Sample Name Item Format

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Example of a 'name' item in the NDJSON export format, representing a Lean identifier.

```json
{"in":1,"str":{"pre":0,"str":"Nat"}}
```

--------------------------------

### Accessing Declarations by Name in Lean

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Example of accessing a constant declaration from the parsed environment using its name.

```lean
if let some constInfo := env.constMap[name]? then
  -- Process constant
```

--------------------------------

### Level.max Format Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/errors.md

This shows the expected JSON format for Level.max, which must be an array of exactly two numbers.

```json
[<left_idx>, <right_idx>]
```

--------------------------------

### Run Lean Exporter Monad

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Executes an exporter computation within the defined monad, starting with a given Lean environment and initial state.

```Lean
def M.run (env : Environment) (act : M α) : IO α
```

```Lean
M.run myEnv do
  initState myEnv
  dumpMetadata
  dumpConstant `Nat
```

--------------------------------

### Metadata Line Format

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Example of the metadata line in the NDJSON export format, including exporter, Lean, and format versions.

```json
{"meta":{"exporter":{"name":"lean4export","version":"3.1.0"},"lean":{"version":"v4.30.0","githash":"hash"},"format":{"version":"3.1.0"}}}
```

--------------------------------

### Lean Toolchain Version

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

The Lean version used for export is determined by the 'lean-toolchain' file in the project. This example specifies Lean version v4.30.0-rc2.

```text
leanprover/lean4:v4.30.0-rc2
```

--------------------------------

### Combine Configuration Options for lean4export

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Demonstrates how to use the lean4export tool with different combinations of configuration flags. The order of flags does not affect the outcome.

```bash
# No options
lake env ../build/bin/lean4export Mathlib

# Single option
lake env ../build/bin/lean4export --export-mdata Mathlib

# Both options
lake env ../build/bin/lean4export --export-mdata --export-unsafe Mathlib

# Order doesn't matter
lake env ../build/bin/lean4export --export-unsafe --export-mdata Mathlib
```

--------------------------------

### Initialize Exporter and Dump Metadata

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Initialize the exporter environment and dump metadata using the Export Monad.

```lean
-- Initialize exporter
let env ← importModules imports {}
M.run env do
  ← initState env opts
  dumpMetadata
  dumpConstant `Nat
```

--------------------------------

### Set up Lean Environment for Exporter

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Execute this command within your project directory to set up the necessary Lean toolchain context for the lean4export binary. It redirects the exporter's output to a file named export.ndjson.

```bash
cd /path/to/project
lake env ../build/bin/lean4export Mathlib > export.ndjson
```

--------------------------------

### Iterating Through Declarations in Export Order

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Demonstrates iterating through all declarations in the environment in the order they appear in the export file.

```lean
env.constOrder.forM fun name =>
  let constInfo := env.constMap[name]!
  -- Process in order
```

--------------------------------

### JSON Format Error Examples

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/errors.md

These examples show valid and invalid JSON objects. The parser expects a JSON object on each line of the NDJSON file.

```json
{"valid": "json"}           # OK
```

```json
{"incomplete": "json"       # Error: Expected JSON object
```

```json
[1, 2, 3]                   # Error: Expected JSON object
```

```json
"just a string"             # Error: Expected JSON object
```

--------------------------------

### initState

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Initializes the exporter's state using provided CLI options and the Lean environment. It configures export flags and performs initial state allocations.

```APIDOC
## initState

### Description
Initializes exporter state from CLI options.

### Method
`def initState (env : Environment) (cliOptions : List String := []) : M Unit`

### Parameters
#### Path Parameters
- `env` (Environment) - Required - Lean environment containing declarations
- `cliOptions` (List String) - Optional - CLI options (see configuration). Defaults to `[]`.

### Side Effects
- Builds `recursorMap` from environment
- Sets `exportMData` and `exportUnsafe` flags
- Performs initial HashMap allocations

### CLI Options Recognized
- `--export-mdata` - Include Expr.mdata in export
- `--export-unsafe` - Export unsafe declarations
```

--------------------------------

### Initialize Exporter State with Options

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

The initState function processes CLI options and initializes the exporter's state. This snippet shows how recursor maps are built and option flags are parsed.

```lean
def initState (env : Environment) (cliOptions : List String := []) : M Unit
```

**Parameters**:

| Parameter | Type | Default | Description |
|-----------|------|---------|-------------|
| `env` | Environment | — | The Lean environment after module import |
| `cliOptions` | `List String` | `[]` | Raw CLI option strings (starting with `--`) |

**Processing Steps**:

1. **Build Recursor Map**
   ```lean
   let mut recursorMap : NameMap NameSet := {}
   for (_, constInfo) in env.constants do
     if let .recInfo recVal := constInfo then
       for indName in recVal.all do
         recursorMap := recursorMap.alter indName (...)
   ```
   Maps each inductive declaration's name to its associated recursor names. Ensures inductive types, constructors, and recursors are exported together.

2. **Parse Option Flags**
   ```lean
   exportMData  := cliOptions.any  (· == "--export-mdata")
   exportUnsafe := cliOptions.any (· == "--export-unsafe")
   ```
   Checks for exact string matches in CLI options.

3. **Update State**
   ```lean
   modify fun st => { st with
     exportMData  := ...
     exportUnsafe := ...
     recursorMap  := ...
   }
   ```

**Side Effects**:
- Builds complete recursor map from environment
- Sets boolean flags in state
- Allocates HashMaps for index tracking

**Return Value**: `M Unit` - Completes in monad context
```

--------------------------------

### Expr.bvar Example

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

This JSON object represents a bound variable using its De Bruijn index.

```json
{"ie": 0, "bvar": 0}
```

--------------------------------

### Configuration Options

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/INDEX.md

Command-line options available for configuring the export process.

```APIDOC
## Configuration Options Reference

### `--export-mdata`

**Type**: Flag
**Default**: false

### `--export-unsafe`

**Type**: Flag
**Default**: false
```

--------------------------------

### Parse BinderInfo from String

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-parse-module.md

Parses binder information from a string. Accepts 'default', 'implicit', 'strictImplicit', or 'instImplicit'. Fails for unknown values.

```lean
def parseBinderInfo (info : String) : M BinderInfo
```

--------------------------------

### Configuration Options

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/INDEX.md

Reference for command-line configuration options for the Lean 4 export module. These flags control whether to export metadata and unsafe definitions.

```Shell
--export-mdata
```

```Shell
--export-unsafe
```

--------------------------------

### Compressing and Decompressing Export Files

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

Commands for compressing and decompressing Lean 4 export files using gzip. Also shows how to stream the export process.

```bash
# Compress export file
gzip -9 export.ndjson

# Decompress
gzip -d export.ndjson.gz

# Stream through pipeline
lake env ../build/bin/lean4export Mathlib | gzip -c > mathlib.ndjson.gz
```

--------------------------------

### Export Module with Options to File

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Exports Mathlib with metadata and unsafe declarations enabled, redirecting output to out.ndjson.

```bash
lake env ../build/bin/lean4export --export-mdata --export-unsafe Mathlib > out.ndjson
```

--------------------------------

### Complete Export Workflow Function

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

The main function orchestrates the export process, including initializing the search path, parsing arguments, importing modules, setting up the environment, and exporting constants with their metadata. It handles both explicit import lists and exporting all non-internal constants.

```lean
def main (args : List String) : IO Unit := do
  initSearchPath (← findSysroot)
  let (opts, args) := args.partition (fun s => s.startsWith "--" && s.length ≥ 3)
  let (imports, constants) := args.span (· != "--")
  let imports := imports.toArray.map fun mod => { module := Syntax.decodeNameLit ("`" ++ mod) |>.get! }
  let env ← importModules imports {}
  let constants := match constants.tail? with
    | some cs => cs.map fun c => Syntax.decodeNameLit ("`" ++ c) |>.get!
    | none    => env.constants.toList.map Prod.fst |>.filter (!·.isInternal)
  M.run env do
    let _ ← initState env opts
    dumpMetadata
    for c in constants do
      modify (fun st => { st with noMDataExprs := {} })
      dumpConstant c
```

--------------------------------

### M.run

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Executes the exporter monad, which combines reader context, mutable state, and IO effects, with a given Lean environment.

```APIDOC
## M.run

### Description
Executes the exporter monad with a given environment.

### Method
`def M.run (env : Environment) (act : M α) : IO α`

### Parameters
#### Path Parameters
- **env** (Environment) - Lean environment to export from
- **act** (M α) - Exporter computation to execute

### Returns
- **IO α** - Result of the computation

### Request Example
```lean
M.run myEnv do
  initState myEnv
  dumpMetadata
  dumpConstant `Nat
```
```

--------------------------------

### Export Module with Default Options

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Invokes lean4export to export the entire Mathlib module with default settings.

```bash
lake env ../build/bin/lean4export Mathlib
```

--------------------------------

### Caching for Faster Exports

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Demonstrates how Lean's compilation caching speeds up subsequent exports of the same module. The second export should be noticeably faster.

```bash
# First time - builds and caches
lake env ../build/bin/lean4export Mathlib > math1.ndjson

# Second time - uses cache
lake env ../build/bin/lean4export Mathlib > math2.ndjson  # Faster
```

--------------------------------

### Export Entire Module

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Use this command to export all declarations from a specified module.

```bash
lake env ../build/bin/lean4export Mathlib > mathlib.ndjson
```

--------------------------------

### Pretty-Print Single Declaration

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Extract the first axiom declaration from the export file and pretty-print it using jq.

```bash
grep '"axiom"' export.ndjson | head -1 | jq '.' 
```

--------------------------------

### Stream and Compress Export

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Export a Lean module and compress the output in a single pipeline, saving it to a .gz file.

```bash
lake env ../build/bin/lean4export Mathlib | gzip -c > mathlib.ndjson.gz
```

--------------------------------

### Troubleshoot Export Failures

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Verify module builds and check constant names when encountering 'Constant not found' errors during export.

```bash
# Verify module builds
lake build

# Check constant name
lake env ../build/bin/lean4export Mathlib -- NonExistentName
```

--------------------------------

### Streaming Parser Implementation in Lean

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

A Lean code snippet demonstrating a streaming parser that processes the export file line by line without loading the entire file into memory.

```lean
def parseFile : M Unit := do
  parseMdata                           -- Read and skip metadata
  loop (← (← get).stream.getLine) do
    parseItem line
    (← get).stream.getLine
```

--------------------------------

### Export Multiple Modules

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Combine exports from multiple modules into a single output file by listing them sequentially.

```bash
lake env ../build/bin/lean4export Mathlib Data -- > combined.ndjson
```

--------------------------------

### lean4export Project File Structure

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/README.md

Lists the main documentation files within the lean4export project, indicating the current file and the purpose of each.

```text
/workspace/home/output/
├── README.md                           ← You are here
├── INDEX.md                            ← Master navigation index
├── quick-reference.md                  ← Command and task reference
├── format-specification.md             ← NDJSON format details
├── api-reference-export-module.md      ← Export API documentation
├── api-reference-parse-module.md       ← Parse API documentation
├── types.md                            ← Type definitions
├── configuration.md                    ← Configuration and options
└── errors.md                           ← Error handling reference

```

--------------------------------

### Convert ReducibilityHints to JSON

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Converts Lean reducibility hints to JSON. The .regular n hint produces a JSON object with a 'regular' key and the natural number n as its value.

```Lean
def Lean.ReducibilityHints.toJson : ReducibilityHints → Json
```

```Lean
ReducibilityHints.opaque.toJson    -- produces: "opaque"
ReducibilityHints.abbrev.toJson    -- produces: "abbrev"
ReducibilityHints.regular 5.toJson -- produces: {"regular": 5}
```

--------------------------------

### Export with Both Metadata and Unsafe Options

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Exports all declarations including metadata and unsafe ones, saving the output to full.ndjson.

```bash
# Both options together
lake env ../build/bin/lean4export --export-mdata --export-unsafe Mathlib > full.ndjson
```

--------------------------------

### Integrate with External Type Checker

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Export Lean library data and then process it with an external type checking tool.

```bash
# Export Lean library
lake env ../build/bin/lean4export Mathlib > export.ndjson

# Parse in external tool
my-type-checker --input export.ndjson --output results.json
```

--------------------------------

### Initialize Exporter State

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Initializes the exporter's state using the provided Lean environment and optional CLI options. It configures flags like `exportMData` and `exportUnsafe`, and builds the `recursorMap`.

```lean
def initState (env : Environment) (cliOptions : List String := []) : M Unit
```

--------------------------------

### Export Multiple Modules with Specific Constants

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Exports specific constants (Nat, Eq) from both Mathlib and Data modules.

```bash
lake env ../build/bin/lean4export Mathlib Data -- Nat Eq
```

--------------------------------

### Print Compressed JSON to Standard Output

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

This line demonstrates how the exporter writes compressed JSON objects to standard output. Each object is formatted on a single line without whitespace.

```lean
IO.println (s.setObjVal! namespaced idx).compress
```

--------------------------------

### Troubleshoot Large Export Files

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Reduce export size by exporting specific modules or constants, and use gzip for compression.

```bash
# Export only specific constants
lake env ../build/bin/lean4export Mathlib -- Nat > nat-only.ndjson

# Compress aggressively
gzip -9 export.ndjson
```

--------------------------------

### Run lean4export with Lake Environment

Source: https://github.com/leanprover/lean4export/blob/master/README.md

Build the lean4export tool using `lake build` and then invoke it via `lake env`. This command exports Lean modules and their dependencies to an NDJSON file.

```sh
lake env <path to lean4export binary> <lean file without .lean suffix>+
```

--------------------------------

### Incremental Updates using lean4export

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Compares the current state of a module with a previous state by exporting both and using the `diff` command. Sorting is used to ensure accurate comparison.

```bash
# Export current state
lake env ../build/bin/lean4export MyModule > current.ndjson

# Export previous state (from git or backup)
lake env ../build/bin/lean4export MyModule > previous.ndjson

# Find differences
diff <(sort current.ndjson) <(sort previous.ndjson)
```

--------------------------------

### Dependency Analysis

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Analyze dependencies by extracting declaration names, sorting them, counting unique occurrences, and displaying the top 20.

```bash
grep '"name"' export.ndjson | sort | uniq -c | sort -rn | head -20
```

--------------------------------

### Troubleshoot JSON Parsing Errors

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Validate JSON format using jq, check the beginning and end of the file, and set LC_ALL to C for cleaner input.

```bash
# Validate JSON format
jq -c '.' export.ndjson > /dev/null

# Check for format issues
head -5 export.ndjson
tail -5 export.ndjson

# Try with cleaner input
export LC_ALL=C
```

--------------------------------

### Minimal Module Export

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

This command exports a single module with default settings, including all non-internal constants and their dependencies. The output is redirected to 'out.ndjson'.

```bash
lake env ../build/bin/lean4export Mathlib > out.ndjson
```

--------------------------------

### Lean4Export Project Layout

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Overview of the lean4export project structure, including key files and directories.

```text
lean4export/
├── Export.lean              # Exporter implementation
├── Export/
│   └── Parse.lean          # Parser implementation
├── Main.lean               # CLI entry point
├── Test.lean               # Tests
├── lakefile.toml           # Lake configuration
├── lean-toolchain          # Lean version
└── format_ndjson.md        # Format specification
```

--------------------------------

### Serialize and Output Metadata

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

The `dumpMetadata` function serializes the metadata and prints it as compressed JSON to standard output. This function must be called before any declarations are exported.

```Lean
def dumpMetadata : M Unit
```

--------------------------------

### Initial Metadata Object

Source: https://github.com/leanprover/lean4export/blob/master/format_ndjson.md

The NDJSON file begins with a metadata object containing version information for the exporter, Lean, and the export format.

```json
{
    "meta": {
        "exporter": {
            "name": string,
            "version": string
            },
        "lean": {
            "githash": string,
            "version": string
        },
        "format": {
            "version": string
        }
    }
}
```

--------------------------------

### Lean.ReducibilityHints.toJson

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Converts reducibility hints into their JSON representation. Handles 'opaque', 'abbrev', and 'regular n' cases.

```APIDOC
## Lean.ReducibilityHints.toJson

### Description
Converts reducibility hints into JSON representation.

### Method
`def Lean.ReducibilityHints.toJson : ReducibilityHints → Json`

### Parameters
#### Input
- **Input** (ReducibilityHints) - ReducibilityHints value

#### Output
- **Output** (Json) - Json value

### Special Cases
- `.regular n` produces object `{"regular": n.toNat}`

### Request Example
```lean
ReducibilityHints.opaque.toJson
ReducibilityHints.abbrev.toJson
ReducibilityHints.regular 5.toJson
```

### Response Example
```json
"opaque"
"abbrev"
{"regular": 5}
```
```

--------------------------------

### Export Module with Metadata and Unsafe Declarations

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Include metadata and unsafe declarations in the export by using the --export-mdata and --export-unsafe flags.

```bash
lake env ../build/bin/lean4export --export-mdata --export-unsafe Mathlib > full.ndjson
```

--------------------------------

### Parse Constructor Declaration Info

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-parse-module.md

Parses constructor declaration information from a JSON object. Requires fields such as name, levelParams, type, parent inductive index, constructor index, and safety status.

```lean
def parseCtorInfo (json : Json) : M Unit
```

--------------------------------

### Compress Exported File

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Create a compressed version of the exported NDJSON file using gzip with maximum compression.

```bash
gzip -9 export.ndjson
```

--------------------------------

### Exporting Free Variables Panic

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/errors.md

This code demonstrates a scenario that would trigger a panic when attempting to export an expression containing free variables. Free variables should not exist in a fully elaborated environment.

```Lean
-- This would trigger if somehow executed
dumpExpr (.fvar `x)  -- panic!
```

--------------------------------

### Convert BinderInfo to JSON

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Converts Lean binder information to its JSON representation. Supported values include default, implicit, strictImplicit, and instImplicit.

```Lean
def Lean.BinderInfo.toJson : BinderInfo → Json
```

```Lean
BinderInfo.default.toJson  -- produces: "default"
BinderInfo.implicit.toJson -- produces: "implicit"
```

--------------------------------

### Parse Level.succ from JSON

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-parse-module.md

Parses a `Level.succ` constructor from JSON. The input is the index of the predecessor level in the `levelMap`.

```lean
def parseLevelSucc (json : Json) : M Level
```

--------------------------------

### Default Export Behavior (Metadata Removed)

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Demonstrates the default behavior where metadata is removed from exported expressions.

```bash
# Default: remove metadata
lake env ../build/bin/lean4export Mathlib > mathlib_no_mdata.ndjson
```

--------------------------------

### Export Module API

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/MANIFEST.txt

Documentation for the Export.lean module, including core exporter functions, type conversions, and metadata export.

```APIDOC
## Export Module API Reference

This section details the API for the `Export.lean` module.

### Core Exporter Functions

- **M.run**
  - Description: Executes the export process.
  - Parameters: Context, State
  - Returns: Exported data

- **initState**
  - Description: Initializes the exporter state.
  - Returns: Initial State object

- **getIdx**
  - Description: Retrieves the current index.
  - Returns: Current index value

- **dumpName**
  - Description: Dumps a Lean name to the output.
  - Parameters: Name

- **dumpLevel**
  - Description: Dumps a Lean level to the output.
  - Parameters: Level

- **dumpUparams**
  - Description: Dumps universe parameters.
  - Parameters: Universe parameters

- **dumpNames**
  - Description: Dumps a collection of Lean names.
  - Parameters: List of Names

- **removeMData**
  - Description: Removes metadata from an export.

- **dumpExprAux**
  - Description: Dumps an expression auxiliary data.
  - Parameters: Expression

- **dumpExpr**
  - Description: Dumps a Lean expression to the output.
  - Parameters: Expression

- **dumpConstant**
  - Description: Dumps a Lean constant to the output.
  - Parameters: Constant name

### Type Conversions

- **BinderInfo**
  - Description: Converts BinderInfo types.

- **ReducibilityHints**
  - Description: Converts ReducibilityHints.

### Context and State

- **Context Structure**
  - Description: Detailed fields for the exporter context.

- **State Structure**
  - Description: Detailed fields for the exporter state.

### Metadata Export

- **Metadata Export Functions**
  - Description: Functions for exporting metadata associated with declarations.
```

--------------------------------

### Metadata Object Structure

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/format-specification.md

The first line of every export file is a metadata object containing version information for the exporter, Lean, and the format itself.

```json
{
  "meta": {
    "exporter": {
      "name": "lean4export",
      "version": "3.1.0"
    },
    "lean": {
      "version": "<lean-version>",
      "githash": "<git-hash>"
    },
    "format": {
      "version": "3.1.0"
    }
  }
}
```

--------------------------------

### Selective Export of Specific Declarations

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

This command exports only the specified declarations (Nat, List, Array, Option) and their dependencies from the Mathlib module. This is useful for exporting only commonly used components.

```bash
lake env ../build/bin/lean4export Mathlib -- Nat List Array Option
```

--------------------------------

### Parallel Exports for Performance

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Exports different modules concurrently using background jobs to improve overall export time. Ensure to use `wait` to synchronize completion.

```bash
# Background jobs
lake env ../build/bin/lean4export Data > data.ndjson &
lake env ../build/bin/lean4export Tactic > tactic.ndjson &
wait
```

--------------------------------

### Export Specific Constants from Module

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Exports only the Nat and Array constants from the Mathlib module.

```bash
lake env ../build/bin/lean4export Mathlib -- Nat Array
```

--------------------------------

### Core Export Functions

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/INDEX.md

Functions for executing the exporter monad, initializing state, and serializing various Lean data structures.

```APIDOC
## Core Export Functions

### `M.run`

**Purpose**: Execute exporter monad.

### `initState`

**Purpose**: Initialize exporter state.

### `getIdx`

**Purpose**: Generate/retrieve primitive index.

### `dumpName`

**Purpose**: Serialize Name.

### `dumpLevel`

**Purpose**: Serialize Level.

### `dumpExpr`

**Purpose**: Serialize Expr.

### `dumpExprAux`

**Purpose**: Low-level expr serialization.

### `removeMData`

**Purpose**: Strip metadata from expressions.

### `dumpConstant`

**Purpose**: Serialize declaration.

### `dumpMetadata`

**Purpose**: Export metadata object.

### `exportMetadata`

**Purpose**: Generate metadata JSON.
```

--------------------------------

### Parse Module API

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/MANIFEST.txt

Documentation for the Export/Parse.lean module, including parsing functions for names, levels, expressions, and declarations.

```APIDOC
## Parse Module API Reference

This section details the API for the `Export/Parse.lean` module.

### Top-Level Parsing Function

- **parseStream**
  - Description: Parses a stream of exported Lean data.
  - Parameters: Input stream
  - Returns: ExportedEnv result

### Index Management Functions

- **8+ Index Management Functions**
  - Description: Functions for managing indices during parsing.

### Parsing Functions

- **Names**
  - **parseNameStr**
    - Description: Parses a name from a string representation.
  - **parseNameNum**
    - Description: Parses a name from a numeric representation.

- **Levels**
  - **parseLevelSucc**
    - Description: Parses a successor level.
  - **parseLevelMax**
    - Description: Parses a maximum level.
  - **Other Level Parsing Functions**
    - Description: Functions for parsing various level constructs.

- **Expressions**
  - **parseExprBVar**
    - Description: Parses a bound variable expression.
  - **parseExprSort**
    - Description: Parses a sort expression.
  - **Other Expression Parsing Functions**
    - Description: Functions for parsing various expression constructs.

- **Declarations**
  - **parseAxiomInfo**
    - Description: Parses axiom information.
  - **parseDefnInfo**
    - Description: Parses definition information.
  - **Other Declaration Parsing Functions**
    - Description: Functions for parsing different types of declarations.

### Item Dispatch Table

- **27 Patterns**
  - Description: Table mapping item types to their parsing functions.

### Error Handling

- **Complete Error Handling Documentation**
  - Description: Details on error reporting and recovery during parsing.
```

--------------------------------

### Inspect Export File Contents

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Provides bash commands to inspect the contents of an export file, including viewing the beginning, end, middle sections, and a random sample.

```bash
# First 10 lines
head -10 export.ndjson

# Last 10 lines
tail -10 export.ndjson

# Middle section
head -100 export.ndjson | tail -50

# Random sample
shuf -n 10 export.ndjson | jq '.'
```

--------------------------------

### Serialize Universe Level with Index Caching

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Serializes a Lean universe `Level` into JSON format with index caching. It supports various level kinds including zero, succ, max, imax, and param, returning the index of the serialized level.

```lean
def dumpLevel (l : Level) : M Nat
```

--------------------------------

### Enable Verbose Output for Debugging

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Activates verbose logging for the lean4export tool by setting the `LEAN_PATH` environment variable and using the `--verbose` flag. This helps in diagnosing issues.

```bash
# Show what's happening
export LEAN_PATH=...
lake env ../build/bin/lean4export --verbose Mathlib
```

--------------------------------

### Export Specific Declarations

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Export only certain constants and their dependencies by listing them after the module name.

```bash
lake env ../build/bin/lean4export Mathlib -- Nat Array List > subset.ndjson
```

--------------------------------

### Default Export Behavior (Unsafe Excluded)

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/configuration.md

Demonstrates the default behavior where unsafe declarations are excluded from the export.

```bash
# Default: exclude unsafe
lake env ../build/bin/lean4export Mathlib > mathlib_safe_only.ndjson
```

--------------------------------

### Compare Two Exports

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Compare two exported NDJSON files by sorting their lines and displaying the first 20 differences.

```bash
diff <(sort export1.ndjson) <(sort export2.ndjson) | head -20
```

--------------------------------

### parseCtorInfo

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-parse-module.md

Parses a constructor declaration from a JSON object. It requires fields for the constructor's name, level parameters, type, parent inductive type, constructor index, number of parameters, number of fields, and whether it is unsafe.

```APIDOC
## parseCtorInfo

### Description
Parses a constructor declaration from a JSON object. It requires fields for the constructor's name, level parameters, type, parent inductive type, constructor index, number of parameters, number of fields, and whether it is unsafe.

### Method
```lean
def parseCtorInfo (json : Json) : M Unit
```

### Parameters
#### JSON Fields Required
- **name** (number) - Constructor name index
- **levelParams** (array) - Level parameters
- **type** (number) - Type expression
- **induct** (number) - Parent inductive name index
- **cidx** (number) - Constructor index
- **numParams** (number) - Number of parameters
- **numFields** (number) - Number of fields
- **isUnsafe** (boolean) - Is unsafe
```

--------------------------------

### Troubleshoot Slow Export Performance

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Improve export performance by ensuring compilation cache is used, exporting specific declarations, or using a machine with more memory.

```bash
# Only export what you need
lake env ../build/bin/lean4export Mathlib -- Nat Array

# Benchmark without redirection
time lake env ../build/bin/lean4export Mathlib > /dev/null
```

--------------------------------

### Lean.BinderInfo.toJson

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Converts Lean binder information into its JSON representation. Supports 'default', 'implicit', 'strictImplicit', and 'instImplicit' values.

```APIDOC
## Lean.BinderInfo.toJson

### Description
Converts Lean binder information into JSON representation.

### Method
`def Lean.BinderInfo.toJson : BinderInfo → Json`

### Parameters
#### Input
- **Input** (BinderInfo) - BinderInfo enumeration

#### Output
- **Output** (Json) - Json value

### Values
- `default`
- `implicit`
- `strictImplicit`
- `instImplicit`

### Request Example
```lean
BinderInfo.default.toJson
BinderInfo.implicit.toJson
```

### Response Example
```json
"default"
"implicit"
```
```

--------------------------------

### Parse Level.imax from JSON

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-parse-module.md

Parses a `Level.imax` constructor from JSON. Expects a JSON array containing two level indices: `[left_index, right_index]`.

```lean
def parseLevelImax (json : Json) : M Level
```

--------------------------------

### Count Declarations by Type

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/quick-reference.md

Count the number of declarations for specific types (Axioms, Definitions, Theorems, Inductives) in the export file.

```bash
# Axioms
grep -c '"axiom"' export.ndjson

# Definitions
grep -c '"def"' export.ndjson

# Theorems
grep -c '"thm"' export.ndjson

# Inductives
grep -c '"inductive"' export.ndjson
```

--------------------------------

### Lean BinderInfo to JSON Conversion

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/types.md

Provides the 'toJson' function for Lean's BinderInfo type, enabling its conversion to a JSON string representation. This is used during the serialization of lambda and forall expressions.

```lean
def Lean.BinderInfo.toJson : BinderInfo → Json
```

--------------------------------

### Serialize Lean Name with Index Caching

Source: https://github.com/leanprover/lean4export/blob/master/_autodocs/api-reference-export-module.md

Serializes a Lean `Name` into JSON format, utilizing index caching for efficiency. It recursively serializes prefix names to build a hierarchical structure and returns the index of the serialized name.

```lean
def dumpName (n : Name) : M Nat
```