Lean Kernel Arena / tutorial/002_badDef

Test "tutorial/002_badDef"

Expected: ✋ reject · Size: 365 B · Lines: 6 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source

Mismatched types

Checker Result ⏱️ 🧠
mathgraph ✋ 1 ms 31.6 MB
sokonanoda ✋ 1 ms 29.6 MB
nanoclo ✋ 1 ms 35.7 MB
con-ron ✋ 23 ms 56.8 MB
lazylean ✋ 1 ms 21.2 MB
nanoda ✋ 0 ms 3.2 MB
nanobruijn ✋ 1 ms 3.5 MB
con-leche ✋ 3 ms 19.6 MB
eink0rn ✋ 1 ms 10.9 MB
ind-models ✋ 58 ms 104.1 MB
official ✋ 27 ms 66.7 MB
lean4lean ✋ 72 ms 103.6 MB
tenet ✋ 99 ms 43.2 MB
nanoclo-fortran ✋ 1 ms 4.4 MB
lean4cobol ✋ 1 ms 13.2 MB
evmlean ✋ 477 ms 132.3 MB
mini ✋ 34 ms 72.9 MB
overfull ✋ 967 ms 45.6 MB
kiota ✋ 1 ms 6.9 MB
canonical-min ✋ 391 ms 1.1 GB
rpylean ✋ 0 ms 4.2 MB
vow-lean-kernel ✋ 42 ms 8.3 MB
official-v4.28.0 ✋ 34 ms 74.0 MB
still-nanoda ✋ 0 ms 3.3 MB
nyaya ✋ 2 ms 8.8 MB
parse-only 👍 27 ms 63.7 MB