# Check

evaluate Lean code and report all messages

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
- **mathlib_options**  
  Enable Mathlib options
- **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