Test "bugs/proj-non-structure"
Expected: ✋ reject · Size: 5.0 KB · Lines: 75 · lean4export: 3.1.0 · Lean: 4.34.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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | ✋ | 1 ms | 40.4 MB | |||
| mathgraph | ✋ | 1 ms | 34.1 MB | |||
| nanoclo | ✋ | 1 ms | 45.9 MB | |||
| con-ron | ✋ | 22 ms | 51.1 MB | |||
| nanobruijn | ✋ | 1 ms | 3.8 MB | |||
| nanoda | ✋ | 1 ms | 3.4 MB | |||
| lazylean | ✋ | 1 ms | 22.0 MB | |||
| con-leche | ✋ | 4 ms | 21.0 MB | |||
| tenet-jvm | ✋ | 103 ms | 65.5 MB | |||
| eink0rn | ✋ | 1 ms | 12.3 MB | |||
| official | ✋ | 28 ms | 67.1 MB | |||
| ind-models | ✋ | 100 ms | 108.5 MB | |||
| lean4lean | ✋ | 28 ms | 98.9 MB | |||
| tenet | ✋ | 131 ms | 44.6 MB | |||
| tenet-hs | ✋ | 1 ms | 8.2 MB | |||
| lean4cobol | ✋ | 3 ms | 13.5 MB | |||
| evmlean | ✋ | 1.2 s | 254.4 MB | |||
| mini | ✋ | 34 ms | 74.7 MB | |||
| overfull | ✋ | 9.3 s | 46.3 MB | |||
| metalean-slow | ✋ | 30 ms | 69.6 MB | |||
| nanoclo-fortran | ✋ | 1 ms | 4.3 MB | |||
| kiota | ✋ | 1 ms | 7.2 MB | |||
| metalean-fast | ✋ | 30 ms | 71.3 MB | |||
| canonical-min | 🚫 | 387 ms | 1.1 GB | |||
| rpylean | ✋ | 0 ms | 4.3 MB | |||
| vow-lean-kernel | 🚫 | 82 ms | 8.3 MB | |||
| parse-only | 👍 | 28 ms | 66.7 MB |