# have2lemma

Extract `have` statements from proofs and convert them into standalone 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.

- `theorems_only` · bool · default: `True` · Process theorems/lemmas only
  - If `true` (default), only `theorem`/`lemma` declarations are processed.

- `include_have_body` · bool · default: `False` · Include proof bodies in extracted lemmas
  - If `true`, extracted lemmas include the original proof. If `false`, they use `sorry` as placeholder.

- `include_whole_context` · bool · default: `True` · Include whole context when extracting
  - If `true`, lemmas include all context variables.

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

- `verbosity` · float · default: `0` · Pretty-printer verbosity level (0-2)
  - 0=default, 1=robust, 2=extra robust.

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

- `environment` · str · required · Lean environment or version
  - The Lean environment to use for evaluation.

- `timeout_seconds` · float · default: `120` · Max execution time in seconds
  - Maximum execution time in seconds.

## 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 have2lemma tool
  - Messages from the have2lemma tool with errors, warnings, and infos lists.

- `content` · string · Lean code with have statements extracted as lemmas
  - The code with `have` statements lifted to top-level lemmas.

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

- `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\nlemma foo.h1 : 1 = 1 := sorry\n\nlemma foo.h2 (h1 : 1 = 1) : 2 = 2 := sorry\n\ntheorem foo : 1 = 1 ∧ 2 = 2 := by\n  have h1 : 1 = 1 := by rfl\n  have h2 : 2 = 2 := by rfl\n  exact ⟨h1, h2⟩",
  "lemma_names": ["foo.h1", "foo.h2"],
  "timings": {
    "total_ms": 95,
    "parse_ms": 88
  }
}
```