# rename

Rename declarations in Lean code.

## Input Parameters

`content` · str · required · Lean source code  
The Lean source code to be processed by this tool.

`declarations` · dict · required · Map from old declaration names to new names  
A dictionary mapping original declaration names to their new names (JSON format).  
All references to renamed declarations are updated throughout the code.

`ignore_imports` · bool · default: `True` · Ignore import mismatches  
Controls import statement handling:

- `true` (default): Ignore the imports in `content` and substitute the environment's default header. This uses the pre-built cached environment, so it is fast. The substituted code is returned in the `content` field.
- `false`: Process the imports in `content` exactly as written. This is significantly slower (the cached environment cannot be reused) and may produce inconsistent or incorrect results if a required dependency such as `Mathlib.Tactic` is missing. A warning is returned in these cases. See the troubleshooting page for more details.

`environment` · str · required · Lean environment or version  
The Lean environment to use for evaluation. Each environment includes a specific  
Lean version and pre-built dependencies (typically Mathlib).

Available environments: `lean-4.28.0`, `lean-4.27.0`, `lean-4.26.0`, etc.

`timeout_seconds` · float · default: `120` · Max execution time in seconds  
Maximum execution time in seconds. Requests exceeding this limit return a timeout error. Note that end-to-end request latency may exceed this timeout due to queue time and other overhead. Additionally, all non-admin requests are subject to an absolute maximum timeout of 900 seconds (15 minutes).

## Output Fields

`lean_messages` · dict · Messages from Lean compiler  
Messages from the Lean compiler with `errors`, `warnings`, and `infos` lists.  
Errors here indicate invalid Lean code (syntax errors, type errors, etc.); an empty `errors` list means the code compiles.

`tool_messages` · dict · Messages from rename tool  
Messages from the rename tool with `errors`, `warnings`, and `infos` lists.  
Errors here indicate tool-specific issues (not Lean compilation errors).

`content` · string · Lean code with renamed declarations  
The Lean code with renamed declarations. The transformed code with all specified declarations renamed. References are updated throughout.

`timings` · dict · Execution timing breakdown  
Timing information in milliseconds for various stages of processing.

## Example Response

```json
{
  "lean_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "content": "import Mathlib\n\ntheorem bar : 1 = 1 := rfl\n\ntheorem baz : 1 = 1 := bar",
  "timings": {
    "total_ms": 94,
    "parse_ms": 89
  }
}
```

## Examples

### Basic rename with reference updates

Renaming `original` → `renamed` also updates all references:

**Before:**
```lean
theorem original : 1 + 1 = 2 := by simp
example : 2 = 1 + 1 := original.symm
```
**After:**
```lean
theorem renamed : 1 + 1 = 2 := by simp
example : 2 = 1 + 1 := renamed.symm
```

### Namespaced declarations

Use fully qualified names (`ns.original`) to rename declarations inside namespaces:

**Before:**
```lean
namespace ns
theorem original : 1 + 1 = 2 := by simp
example : 2 = 1 + 1 := original.symm
end ns

example : 2 = 1 + 1 := ns.original.symm
```
**After** (with `{"ns.original": "ns.renamed"}`):
```lean
namespace ns
theorem renamed : 1 + 1 = 2 := by simp
example : 2 = 1 + 1 := renamed.symm
end ns

example : 2 = 1 + 1 := ns.renamed.symm
```

### Renaming inductive types

Renaming an inductive type also updates constructor references:

**Before:**
```lean
inductive enum
| caseA
| caseB

example : enum := enum.caseA
```
**After** (with `{"enum": "caseEnum"}`):
```lean
inductive caseEnum
| caseA
| caseB

example : caseEnum := caseEnum.caseA
```