Test "tutorial/097_projIndexData2"
Expected: ✋ reject · Size: 14.1 KB · Lines: 226 · lean4export: 3.1.0 · Lean: 4.34.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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | ✋ | 1 ms | 40.0 MB | |||
| mathgraph | ✋ | 1 ms | 37.7 MB | |||
| nanoclo | ✋ | 1 ms | 43.8 MB | |||
| con-ron | ✋ | 24 ms | 60.9 MB | |||
| nanobruijn | ✋ | 1 ms | 12.0 MB | |||
| nanoda | ✋ | 1 ms | 3.0 MB | |||
| lazylean | ✋ | 1 ms | 21.6 MB | |||
| con-leche | ✋ | 4 ms | 20.1 MB | |||
| eink0rn | ✋ | 2 ms | 13.0 MB | |||
| official | ✋ | 29 ms | 67.2 MB | |||
| ind-models | ✋ | 101 ms | 105.4 MB | |||
| lean4lean | ✋ | 29 ms | 98.2 MB | |||
| tenet | ✋ | 136 ms | 45.2 MB | |||
| tenet-hs | ✋ | 2 ms | 10.2 MB | |||
| lean4cobol | ✋ | 8 ms | 13.7 MB | |||
| evmlean | ✋ | 2.0 s | 255.9 MB | |||
| mini | ✋ | 35 ms | 73.7 MB | |||
| overfull | ✋ | 32.2 s | 47.1 MB | |||
| metalean-slow | ✋ | 31 ms | 75.7 MB | |||
| tenet-jvm | ✋ | 123 ms | 64.7 MB | |||
| nanoclo-fortran | ✋ | 1 ms | 4.4 MB | |||
| kiota | ✋ | 1 ms | 9.4 MB | |||
| metalean-fast | ✋ | 31 ms | 74.2 MB | |||
| canonical-min | 🚫 | 387 ms | 1.1 GB | |||
| rpylean | ✋ | 1 ms | 4.6 MB | |||
| vow-lean-kernel | ✋ | 124 ms | 8.4 MB | |||
| parse-only | 👍 | 28 ms | 66.0 MB |