Test "init-prelude"
Expected: 👍 accept · Size: 3.5 MB · Lines: 63.7 k · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
The Init.Prelude module export.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| nanoda | 👍 | 154 ms | (-62%) | 8.3 MB | ||
| nanobruijn | 👍 | 221 ms | (-45%) | 32.5 MB | ||
| official-nightly | 👍 | 389 ms | (-4%) | 64.3 MB | ||
| official | 👍 | 403 ms | (0%) | 73.0 MB | ||
| official-v4.28.0 | 👍 | 419 ms | (+4%) | 75.9 MB | ||
| mini | 🚫 | 49 ms | 70.3 MB | |||
| evmlean | 🚫 | 359 ms | 88.1 MB | |||
| always-decline | 🚫 | 1 ms | 2.8 MB | |||
| lean4lean | 👍 | 513 ms | (+27%) | 99.1 MB | ||
| still-nanoda | 👍 | 153 ms | (-62%) | 8.0 MB | ||
| rpylean | 👍 | 219 ms | (-46%) | 114.6 MB | ||
| always-reject | ✋ | 1 ms | 2.8 MB | |||
| sokonanoda | 👍 | 153 ms | (-62%) | 10.3 MB | ||
| parse-only | 👍 | 256 ms | (-37%) | 76.0 MB | ||
| always-accept | 👍 | 1 ms | (-100%) | 2.8 MB |