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) | 200.4 MB | (×2.7) | |
| mathgraph | 👍 | 37 ms | (÷9.8) | 139.9 MB | (+90%) | |
| nanoclo | 👍 | 90 ms | (÷4.0) | 91.9 MB | (+25%) | |
| con-ron | 👍 | 239 ms | (-34%) | 103.1 MB | (+40%) | |
| nanobruijn | 👍 | 213 ms | (-41%) | 32.1 MB | (÷2.3) | |
| nanoda | 👍 | 145 ms | (÷2.5) | 8.6 MB | (÷8.6) | |
| lazylean | 👍 | 101 ms | (÷3.6) | 29.4 MB | (÷2.5) | |
| con-leche | 👍 | 462 ms | (+28%) | 30.6 MB | (÷2.4) | |
| eink0rn | 👍 | 232 ms | (-36%) | 267.8 MB | (×3.6) | |
| official | 👍 | 362 ms | (0%) | 73.7 MB | (0%) | |
| ind-models | 👍 | 869 ms | (×2.4) | 131.7 MB | (+79%) | |
| lean4lean | 👍 | 433 ms | (+20%) | 106.1 MB | (+44%) | |
| tenet | 👍 | 567 ms | (+57%) | 128.5 MB | (+74%) | |
| tenet-hs | 👍 | 256 ms | (-29%) | 79.1 MB | (+7%) | |
| lean4cobol | 👍 | 3.3 s | (×9.2) | 21.6 MB | (÷3.4) | |
| evmlean | 🚫 | 0 ms | 0 B | |||
| mini | 🚫 | 0 ms | 0 B | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 🚫 | 1.1 s | 79.5 MB | |||
| tenet-jvm | 👍 | 1.6 s | (×4.4) | 174.8 MB | (×2.4) | |
| nanoclo-fortran | 👍 | 229 ms | (-37%) | 19.0 MB | (÷3.9) | |
| kiota | 👍 | 199 ms | (-45%) | 61.4 MB | (-17%) | |
| metalean-fast | 👍 | 629 ms | (+74%) | 98.7 MB | (+34%) | |
| canonical-min | ✋ | 605 ms | 1.1 GB | |||
| rpylean | 👍 | 163 ms | (÷2.2) | 56.4 MB | (-24%) | |
| vow-lean-kernel | 👍 | 16.3 s | (×45) | 34.4 MB | (÷2.1) | |
| parse-only | 👍 | 222 ms | (-39%) | 74.0 MB | (0%) |