# Replace Have Statements with Sorry

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

Use [extract_decl](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

**theorems_only**  
Process theorems/lemmas only

**timeout_seconds**  
Max execution time in seconds

RUNCLEAR

## Result

Shareable Link

API Call

FILE A BUG