Test "tutorial/097_projIndexData2"
Expected: ✋ reject · Size: 6.8 KB · Lines: 111 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source
Projecting out data is not allowed, even if this data appears as an index and the recursor would allow it.
This also forbids projecting out proofs that follow such fields.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | ✋ | 1 ms | 33.9 MB | |||
| nanoda | ✋ | 1 ms | 3.1 MB | |||
| nanobruijn | ✋ | 1 ms | 8.8 MB | |||
| ind-models | ✋ | 58 ms | 105.1 MB | |||
| official | ✋ | 28 ms | 66.6 MB | |||
| lean4lean | ✋ | 28 ms | 97.1 MB | |||
| evmlean | ✋ | 783 ms | 133.3 MB | |||
| mini | ✋ | 34 ms | 73.8 MB | |||
| sokonanoda | ✋ | 1 ms | 34.0 MB | |||
| nanoclo | ✋ | 1 ms | 41.5 MB | |||
| zignodamus | ✋ | 1 ms | 4.8 MB | |||
| vow-lean-kernel | ✋ | 84 ms | 8.1 MB | |||
| official-v4.28.0 | ✋ | 35 ms | 73.9 MB | |||
| still-nanoda | ✋ | 1 ms | 3.0 MB | |||
| kiota | ✋ | 1 ms | 6.8 MB | |||
| rpylean | ✋ | 1 ms | 8.3 MB | |||
| nyaya | ✋ | 2 ms | 9.4 MB | |||
| parse-only | 👍 | 27 ms | 65.4 MB |