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.8 MB | |||
| sokonanoda | ✋ | 1 ms | 33.7 MB | |||
| nanoclo | ✋ | 1 ms | 49.6 MB | |||
| con-ron | ✋ | 23 ms | 60.7 MB | |||
| lazylean | ✋ | 1 ms | 21.3 MB | |||
| nanoda | ✋ | 1 ms | 3.2 MB | |||
| nanobruijn | ✋ | 1 ms | 9.3 MB | |||
| con-leche | ✋ | 4 ms | 17.7 MB | |||
| eink0rn | ✋ | 2 ms | 11.6 MB | |||
| ind-models | ✋ | 58 ms | 104.7 MB | |||
| official | ✋ | 28 ms | 67.0 MB | |||
| lean4lean | ✋ | 28 ms | 98.4 MB | |||
| tenet | ✋ | 133 ms | 44.4 MB | |||
| nanoclo-fortran | ✋ | 1 ms | 4.6 MB | |||
| lean4cobol | ✋ | 4 ms | 13.4 MB | |||
| evmlean | ✋ | 787 ms | 133.0 MB | |||
| mini | ✋ | 34 ms | 71.0 MB | |||
| overfull | ✋ | 13.7 s | 46.2 MB | |||
| kiota | ✋ | 1 ms | 7.0 MB | |||
| canonical-min | 🚫 | 387 ms | 1.1 GB | |||
| rpylean | ✋ | 1 ms | 4.4 MB | |||
| vow-lean-kernel | ✋ | 84 ms | 8.4 MB | |||
| official-v4.28.0 | ✋ | 35 ms | 74.1 MB | |||
| still-nanoda | ✋ | 1 ms | 3.1 MB | |||
| nyaya | ✋ | 2 ms | 9.1 MB | |||
| parse-only | 👍 | 27 ms | 65.8 MB |