Test "init"
Expected: 馃憤 accept 路 Size: 309.5鈥疢B 路 Lines: 6.1鈥疢 路 lean4export: 3.1.0 路 Lean: 4.29.1 路 Timeout: 8.3鈥痬 路 馃搫 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 | 馃憤 | 6.1鈥痵 | (梅10.0) | 571.7鈥疢B | (+6%) | |
| sokonanoda | 馃憤 | 6.5鈥痵 | (梅9.4) | 690.3鈥疢B | (+28%) | |
| nanoclo | 馃憤 | 20.2鈥痵 | (梅3.0) | 571.6鈥疢B | (+6%) | |
| con-ron | 馃憤 | 31.6鈥痵 | (-48%) | 697.2鈥疢B | (+30%) | |
| lazylean | 馃憤 | 35.5鈥痵 | (-42%) | 374.0鈥疢B | (-30%) | |
| nanoda | 馃憤 | 34.4鈥痵 | (-44%) | 409.3鈥疢B | (-24%) | |
| nanobruijn | 馃憤 | 34.2鈥痵 | (-44%) | 436.5鈥疢B | (-19%) | |
| con-leche | 馃憤 | 1.2鈥痬 | (+21%) | 522.7鈥疢B | (-3%) | |
| eink0rn | 馃憤 | 43.3鈥痵 | (-29%) | 980.4鈥疢B | (+82%) | |
| ind-models | 馃憤 | 1.2鈥痬 | (+19%) | 517.9鈥疢B | (-4%) | |
| official | 馃憤 | 1.0鈥痬 | (0%) | 537.9鈥疢B | (0%) | |
| lean4lean | 馃憤 | 1.5鈥痬 | (+44%) | 584.3鈥疢B | (+9%) | |
| tenet | 馃憤 | 1.1鈥痬 | (+9%) | 2.5鈥疓B | (脳4.8) | |
| nanoclo-fortran | 馃憤 | 1.1鈥痬 | (+5%) | 982.0鈥疢B | (+83%) | |
| lean4cobol | 馃憤 | 13.9鈥痬 | (脳14) | 497.6鈥疢B | (-7%) | |
| evmlean | 馃毇 | 0鈥痬s | 0鈥疊 | |||
| mini | 馃毇 | 0鈥痬s | 0鈥疊 | |||
| overfull | 馃挜 | 1.5鈥痬 | 46.9鈥疢B | |||
| kiota | 馃毇 | 2.1鈥痬 | 1004.1鈥疢B | |||
| canonical-min | 馃毇 | 18.5鈥痵 | 1.5鈥疓B | |||
| rpylean | 馃憤 | 2.1鈥痬 | (脳2.1) | 3.5鈥疓B | (脳6.7) | |
| vow-lean-kernel | 馃挜 | 1.2鈥痬 | 442.1鈥疢B | |||
| official-v4.28.0 | 馃憤 | 1.6鈥痬 | (+53%) | 562.6鈥疢B | (+5%) | |
| still-nanoda | 馃憤 | 46.1鈥痵 | (-25%) | 405.7鈥疢B | (-25%) | |
| nyaya | 馃挜 | 16.0鈥痵 | 686.6鈥疢B | |||
| parse-only | 馃憤 | 16.4鈥痵 | (梅3.7) | 534.9鈥疢B | (-1%) |