Test "init"
Expected: 👍 accept · Size: 309.5 MB · Lines: 6.1 M · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source
The Init module export from Lean 4 core.
This test contains the fundamental building blocks of Lean 4, including:
- Basic data types (Nat, List, Array, String, etc.)
- Core tactics and syntax
- Foundational mathematical structures
- Essential metaprogramming infrastructure
This is one of the smallest meaningful test cases, making it ideal for initial checker validation and debugging.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 8.1 s | (÷8.3) | 738.1 MB | (+35%) | |
| ind-models | 👍 | 1.2 m | (+8%) | 515.3 MB | (-6%) | |
| official-nightly | 👍 | 1.0 m | (-9%) | 532.8 MB | (-3%) | |
| evmlean | 🚫 | 0 ms | 0 B | |||
| nanoda | 👍 | 34.6 s | (-49%) | 401.3 MB | (-27%) | |
| mini | 🚫 | 0 ms | 0 B | |||
| lean4lean | 👍 | 1.5 m | (+31%) | 584.5 MB | (+7%) | |
| sokonanoda | 👍 | 9.0 s | (÷7.5) | 672.3 MB | (+23%) | |
| zignodamus | 👍 | 13.4 s | (÷5.0) | 757.2 MB | (+38%) | |
| nanoclo | 👍 | 20.2 s | (÷3.3) | 582.8 MB | (+6%) | |
| nanobruijn | 👍 | 35.4 s | (-47%) | 437.9 MB | (-20%) | |
| kiota | ✋ | 5.6 m | 11.9 GB | |||
| official | 👍 | 1.1 m | (0%) | 548.7 MB | (0%) | |
| vow-lean-kernel | 💥 | 1.4 m | 486.6 MB | |||
| rpylean | 👍 | 2.2 m | (+93%) | 3.4 GB | (×6.3) | |
| official-v4.28.0 | 👍 | 1.6 m | (+39%) | 561.6 MB | (+2%) | |
| still-nanoda | 👍 | 46.1 s | (-31%) | 421.1 MB | (-23%) | |
| nyaya | 💥 | 16.0 s | 687.1 MB | |||
| parse-only | 👍 | 16.6 s | (÷4.0) | 534.1 MB | (-3%) |