Test "std"
Expected: 馃憤 accept 路 Size: 526.1鈥疢B 路 Lines: 10.0鈥疢 路 lean4export: 3.1.0 路 Lean: 4.29.1 路 馃搫 Declaration 路 馃敆 Source
The complete Std library export from Lean 4.
This test contains the standard library extensions beyond core Lean 4, including:
- Enhanced data structures (HashMap, RBTree, etc.)
- Additional mathematical operations
- Extended list and array operations
- Utility functions and theorems
This represents a medium-sized test case, larger than core modules but smaller than Mathlib, making it useful for performance testing.
| Checker | Result | 鈴憋笍 | 馃 | |||
|---|---|---|---|---|---|---|
| mathgraph | 馃憤 | 13.1鈥痵 | (梅8.6) | 1.1鈥疓B | (+8%) | |
| ind-models | 馃憤 | 2.1鈥痬 | (+10%) | 863.2鈥疢B | (-14%) | |
| official-nightly | 馃憤 | 1.7鈥痬 | (-9%) | 872.3鈥疢B | (-13%) | |
| evmlean | 馃毇 | 0鈥痬s | 0鈥疊 | |||
| nanoda | 馃憤 | 55.0鈥痵 | (梅2.1) | 662.7鈥疢B | (-34%) | |
| mini | 馃毇 | 0鈥痬s | 0鈥疊 | |||
| lean4lean | 馃憤 | 2.3鈥痬 | (+23%) | 995.9鈥疢B | (-1%) | |
| sokonanoda | 馃憤 | 14.3鈥痵 | (梅7.9) | 1.1鈥疓B | (+10%) | |
| zignodamus | 馃憤 | 20.7鈥痵 | (梅5.5) | 1.1鈥疓B | (+11%) | |
| nanoclo | 馃憤 | 33.6鈥痵 | (梅3.4) | 900.1鈥疢B | (-10%) | |
| nanobruijn | 馃憤 | 59.7鈥痵 | (-47%) | 709.3鈥疢B | (-29%) | |
| kiota | 馃挜 | 23.0鈥痬 | 14.2鈥疓B | |||
| official | 馃憤 | 1.9鈥痬 | (0%) | 1005.2鈥疢B | (0%) | |
| vow-lean-kernel | 馃挜 | 1.4鈥痬 | 480.1鈥疢B | |||
| rpylean | 馃憤 | 27.4鈥痬 | (脳15) | 7.1鈥疓B | (脳7.2) | |
| official-v4.28.0 | 馃憤 | 2.5鈥痬 | (+34%) | 1021.8鈥疢B | (+2%) | |
| still-nanoda | 馃憤 | 1.1鈥痬 | (-40%) | 650.6鈥疢B | (-35%) | |
| nyaya | 馃毇 | 0鈥痬s | 0鈥疊 | |||
| parse-only | 馃憤 | 28.2鈥痵 | (梅4.0) | 938.9鈥疢B | (-7%) |