Test "init-prelude"
Expected: 👍 accept · Size: 3.6 MB · Lines: 64.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 50.0 s · 📄 Declaration · 🔗 Source
The Init.Prelude module export.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | 👍 | 30 ms | (÷12) | 204.3 MB | (×2.8) | |
| mathgraph | 👍 | 37 ms | (÷9.8) | 135.9 MB | (+84%) | |
| nanoclo | 👍 | 90 ms | (÷4.0) | 91.5 MB | (+24%) | |
| con-ron | 👍 | 239 ms | (-34%) | 100.8 MB | (+37%) | |
| nanobruijn | 👍 | 213 ms | (-41%) | 32.3 MB | (÷2.3) | |
| lazylean | 👍 | 101 ms | (÷3.6) | 28.4 MB | (÷2.6) | |
| nanoda | 👍 | 145 ms | (÷2.5) | 8.3 MB | (÷8.9) | |
| con-leche | 👍 | 462 ms | (+28%) | 30.1 MB | (÷2.4) | |
| eink0rn | 👍 | 232 ms | (-36%) | 268.5 MB | (×3.6) | |
| official | 👍 | 362 ms | (0%) | 73.8 MB | (0%) | |
| ind-models | 👍 | 868 ms | (×2.4) | 133.7 MB | (+81%) | |
| lean4lean | 👍 | 433 ms | (+20%) | 104.1 MB | (+41%) | |
| tenet | 👍 | 568 ms | (+57%) | 127.9 MB | (+73%) | |
| nanoclo-fortran | 👍 | 229 ms | (-37%) | 19.4 MB | (÷3.8) | |
| lean4cobol | 👍 | 3.3 s | (×9.2) | 21.4 MB | (÷3.5) | |
| evmlean | 🚫 | 0 ms | 0 B | |||
| mini | 🚫 | 0 ms | 0 B | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 🚫 | 1.1 s | 80.1 MB | |||
| kiota | 👍 | 199 ms | (-45%) | 61.1 MB | (-17%) | |
| metalean-fast | 👍 | 629 ms | (+74%) | 96.1 MB | (+30%) | |
| canonical-min | ✋ | 605 ms | 1.1 GB | |||
| rpylean | 👍 | 164 ms | (÷2.2) | 56.1 MB | (-24%) | |
| vow-lean-kernel | 👍 | 16.3 s | (×45) | 33.8 MB | (÷2.2) | |
| parse-only | 👍 | 222 ms | (-39%) | 73.8 MB | (0%) |