# sorry2lemma

Extract `sorry` placeholders and unsolved goals at error locations from Lean code and lift them into standalone top-level lemmas.

## Input Parameters

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

- `names` · list[str] · Theorem names to process  
  Optional list of theorem names to process. If not specified, all theorems are processed.

- `indices` · list[int] · Theorem indices to process  
  Optional list of theorem indices to process (0-based). Supports negative indices: `-1` is the last theorem, `-2` is second-to-last, etc.

- `extract_sorries` · bool · default: `True` · Lift sorries into standalone lemmas  
  If `true`, `sorry` placeholders are extracted into standalone lemmas. Defaults to true.

- `extract_errors` · bool · default: `True` · Lift errors into standalone lemmas  
  If `true`, error positions (type mismatches, etc.) are extracted into standalone lemmas. Defaults to true.

- `include_whole_context` · bool · default: `True` · Include whole context when extracting  
  If `true`, lemmas include all context variables. If `false`, attempts to minimize the context. Defaults to true.

- `reconstruct_callsite` · bool · default: `False` · Replace sorry with lemma call  
  If `true`, the original `sorry` is replaced with a call to the extracted lemma. Defaults to false.

- `merge_duplicates` · bool · default: `False` · Merge duplicate extracted lemmas  
  If `true`, extracted lemmas within the same parent that are definitionally equal — to each other, or to the `theorem`/`lemma` they were extracted from — are merged: duplicates collapse into a single lemma that all callsites reference, and a sorry whose goal is definitionally equal to its parent theorem/lemma is dropped rather than lifted into a restatement. Defaults to false.

- `theorems_only` · bool · default: `True` · Process theorems/lemmas only  
  If `true` (default), only `theorem`/`lemma` declarations are processed. Set to `false` to process all declaration kinds. When `false`, `names` and `indices` select over all declarations rather than just theorems.

- `verbosity` · float · default: `0` · Pretty-printer verbosity level (0-2)  
  0=default, 1=robust, 2=extra robust. Higher levels produce more explicit type annotations. Use when default output has ambiguity errors.

- `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.  
  - `false`: Process the imports in `content` exactly as written.

- `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.

- `timeout_seconds` · float · default: `120` · Max execution time in seconds  
  Maximum execution time in seconds. Requests exceeding this limit return a timeout error.

## Output Fields

- `lean_messages` · dict · Messages from Lean compiler  
  Messages from the Lean compiler with `errors`, `warnings`, and `infos` lists.

- `tool_messages` · dict · Messages from sorry2lemma tool  
  Messages from the sorry2lemma tool with `errors`, `warnings`, and `infos` lists.

- `content` · string · Lean code with sorries/errors extracted as lemmas  
  The code with `sorry` and error positions lifted to top-level lemmas with their goals as types.

- `lemma_names` · list · Names of newly created lemmas  
  Names are auto-generated based on the parent theorem and position.

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

## Example Response

```json
{
  "lean_messages": {
    "errors": [],
    "warnings": ["-:3:6-3:11: warning: declaration uses 'sorry'\n", "-:5:8-5:13: warning: declaration uses 'sorry'\n"],
    "infos": []
  },
  "tool_messages": {
    "errors": [],
    "warnings": [],
    "infos": []
  },
  "content": "import Mathlib\n\nlemma foo.sorried (p q : Prop) (hp : p) : q := sorry\n\ntheorem foo (p q : Prop) : p → q := by\n  intro hp\n  sorry",
  "lemma_names": ["foo.sorried"],
  "timings": {
    "total_ms": 95,
    "parse_ms": 88
  }
}
```

The `sorry2lemma` tool extracts `sorry` placeholders and unsolved goals at error locations into standalone lemmas.