Test "bugs/proj-non-structure"
Expected: ✋ reject · Size: 5.0 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source
Bad has two constructors, so projections should not be allowed.
Prove false by using the second constructor, then projecting, hoping that the
first constructor is used when inferring the type of the projection.
Nanoda and its descendants accepted this until it was fixed.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | ✋ | 1 ms | 33.8 MB | |||
| sokonanoda | ✋ | 1 ms | 33.7 MB | |||
| nanoclo | ✋ | 1 ms | 43.7 MB | |||
| con-ron | 🚫 | 23 ms | 58.8 MB | |||
| lazylean | ✋ | 1 ms | 21.2 MB | |||
| nanoda | ✋ | 1 ms | 3.1 MB | |||
| nanobruijn | ✋ | 1 ms | 3.4 MB | |||
| con-leche | 🚫 | 4 ms | 20.1 MB | |||
| eink0rn | ✋ | 2 ms | 11.5 MB | |||
| ind-models | ✋ | 58 ms | 105.1 MB | |||
| official | ✋ | 28 ms | 66.9 MB | |||
| lean4lean | ✋ | 28 ms | 98.6 MB | |||
| tenet | ✋ | 131 ms | 44.2 MB | |||
| nanoclo-fortran | ✋ | 1 ms | 4.3 MB | |||
| lean4cobol | ✋ | 3 ms | 13.6 MB | |||
| evmlean | ✋ | 676 ms | 132.2 MB | |||
| mini | ✋ | 34 ms | 73.5 MB | |||
| overfull | ✋ | 9.3 s | 45.9 MB | |||
| kiota | ✋ | 1 ms | 7.0 MB | |||
| canonical-min | 🚫 | 386 ms | 1.1 GB | |||
| rpylean | ✋ | 0 ms | 4.4 MB | |||
| vow-lean-kernel | 🚫 | 83 ms | 8.5 MB | |||
| official-v4.28.0 | ✋ | 34 ms | 74.3 MB | |||
| still-nanoda | 👍 | 1 ms | 3.2 MB | |||
| nyaya | ✋ | 2 ms | 9.0 MB | |||
| parse-only | 👍 | 27 ms | 65.0 MB |