Lean Kernel Arena / con-agua / other/sparse-name-index

Checker "con-agua" on test "other/sparse-name-index"

Checker: con-agua · Version: 7166eda · 📄 Declaration · 🔗 Source

Test: other/sparse-name-index · Expected: 👍 accept · Size: 292 B · Lines: 4 · lean4export: 0.1.0 · Lean: 4.29.1 · 📄 Declaration

Result: 🚫 declined · exit code 2 · wall time: 14.7 ms · instructions: 105.8 M · max rss memory: 8.4 MB · run 2026-10-27 00:34:48 UTC

stdout:
declined: non-standard axiom (…); con-leche does not support such axioms at the moment