rename¶

Rename declarations in Lean code.

Python API¶

result = await axle.rename(
    content="import Mathlib\ntheorem foo : 1 = 1 := rfl\ntheorem baz : 1 = 1 := foo",
    declarations={"foo": "bar"},
    environment="lean-4.26.0",
    timeout_seconds=120,  # Optional
)
print(result.content)  # theorem bar : 1 = 1 := rfl

CLI¶

Usage: axle rename CONTENT [OPTIONS]

# Rename using command-line mapping
axle rename theorem.lean --declarations foo=bar,helper=main_helper --environment lean-4.26.0
# Rename using JSON file
axle rename theorem.lean --declarations-file mapping.json --environment lean-4.26.0
# Save to file
axle rename theorem.lean --declarations foo=bar -o renamed.lean --environment lean-4.26.0
# Pipeline usage
cat theorem.lean | axle rename - --declarations foo=bar --environment lean-4.26.0 | axle check - --environment lean-4.26.0

HTTP API¶

curl -s -X POST http://10.1.10.100:8989/v1/axle/rename \
    -d '{"content": "import Mathlib\ntheorem foo : 1 = 1 := rfl\ntheorem baz : 1 = 1 := foo", "declarations": {"foo": "bar"}, "environment": "lean-4.26.0"}' | jq

Input Parameters¶

Name	Type	Required	Description
`content`	`str`	Yes	A string of Lean code
`declarations`	`dict[str, str]`	Yes	Map from old declaration names to new names
`environment`	`str`	Yes	Environment to use (e.g., `"lean-4.26.0"`, `"lean-4.25.1"`)
`ignore_imports`	`bool`	No	If true, ignore import statement mismatches and use the environment's default imports. If false, raise an error on mismatch. Default: false
`timeout_seconds`	`float`	No	Maximum execution time (default: 120)

Note: Renames are NOT transitive. If A is renamed to B and B is renamed to C, then A will end up as B, not C.

Output Fields¶

Name	Type	Description
`lean_messages`	`dict`	Messages from Lean compiler with `errors`, `warnings`, `infos` lists
`tool_messages`	`dict`	Messages from rename tool with `errors`, `warnings`, `infos` lists
`content`	`str`	The Lean code with renamed declarations
`timings`	`dict`	Timing info: `total_ms`, `parse_ms`

Example Response¶

{
  "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
  }
}

Demo¶

Simple¶

theorem original : True := trivial

→

theorem renamed : True := trivial

Dot notation¶

theorem original : 1 + 1 = 2 := by simp
example : 2 = 1 + 1 := original.symm

→

theorem renamed : 1 + 1 = 2 := by simp
example : 2 = 1 + 1 := renamed.symm

Namespaces¶

namespace ns

theorem original : 1 + 1 = 2 := by simp
example : 2 = 1 + 1 := original.symm

end ns

example : 2 = 1 + 1 := ns.original.symm

→

namespace ns

theorem renamed : 1 + 1 = 2 := by simp
example : 2 = 1 + 1 := renamed.symm

end ns

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

Constructors and Projections¶

inductive enum
| caseA
| caseB

example : enum := enum.caseA

→

inductive caseEnum
| caseA
| caseB

example : caseEnum := caseEnum.caseA