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

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