# Extract Sorries and Errors to Lemmas

This tool is deprecated and will be removed in a future release.

Use [extract_decls](https://axle.axiommath.ai/extract_decls) instead, which supports all declaration kinds.

## Input

- **environment***  
  Lean environment or version  
  `lean-4.32.0`, `lean-4.31.0`, `lean-4.30.0`, `lean-4.29.0`, `lean-4.28.0`, `lean-4.27.0`, `lean-4.26.0`, `lean-4.25.1`, `lean-4.24.0`, `lean-4.23.0`, `lean-4.22.0`, `lean-4.21.0`

- **ignore_imports**  
  Ignore import mismatches  
  Default header (injected when enabled):  
  ```
  import Mathlib
  ```

- **content***  
  Lean source code

- **names**  
  Theorem names to process

- **indices**  
  Theorem indices to process

- **extract_sorries**  
  Lift sorries into standalone lemmas

- **extract_errors**  
  Lift errors into standalone lemmas

- **include_whole_context**  
  Include whole context when extracting

- **reconstruct_callsite**  
  Replace sorry with lemma call

- **merge_duplicates**  
  Merge duplicate extracted lemmas (by definitional equality)

- **theorems_only**  
  Process theorems/lemmas only

- **verbosity**  
  Pretty-printer verbosity level (0-2)

- **timeout_seconds**  
  Max execution time in seconds

## Result

- **Shareable Link**  
- **API Call**  
- **FILE A BUG**