Lean Kernel Arena / tutorial/101_ruleKAcc

Test "tutorial/101_ruleKAcc"

Expected: ✋ reject · Size: 12.8 KB · Lines: 238 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Rule k should not fire for Acc.

Checker Result ⏱️ 🧠
mathgraph ✋ 1 ms 37.9 MB
sokonanoda ✋ 1 ms 35.7 MB
nanoclo ✋ 1 ms 49.8 MB
con-ron ✋ 23 ms 60.5 MB
lazylean ✋ 2 ms 21.3 MB
nanoda ✋ 1 ms 3.1 MB
nanobruijn ✋ 1 ms 10.4 MB
con-leche ✋ 4 ms 20.1 MB
eink0rn ✋ 2 ms 12.6 MB
ind-models ✋ 60 ms 105.5 MB
official ✋ 30 ms 66.7 MB
lean4lean ✋ 77 ms 104.1 MB
tenet ✋ 136 ms 44.5 MB
nanoclo-fortran ✋ 2 ms 4.4 MB
lean4cobol ✋ 9 ms 13.7 MB
evmlean ✋ 2.7 s 131.6 MB
mini ✋ 43 ms 71.7 MB
overfull ✋ 37.3 s 47.1 MB
kiota ✋ 1 ms 9.1 MB
canonical-min ✋ 388 ms 1.1 GB
rpylean ✋ 1 ms 5.0 MB
vow-lean-kernel ✋ 92 ms 8.4 MB
official-v4.28.0 ✋ 36 ms 75.0 MB
still-nanoda ✋ 1 ms 3.1 MB
nyaya ✋ 3 ms 9.8 MB
parse-only 👍 28 ms 65.6 MB