Test "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.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | ✋ | 1 ms | 33.9 MB | |||
| ind-models | ✋ | 58 ms | 104.1 MB | |||
| official-nightly | ✋ | 28 ms | 64.3 MB | |||
| evmlean | ✋ | 675 ms | 133.2 MB | |||
| nanoda | ✋ | 1 ms | 3.1 MB | |||
| mini | ✋ | 34 ms | 69.8 MB | |||
| lean4lean | ✋ | 28 ms | 94.8 MB | |||
| sokonanoda | ✋ | 1 ms | 34.0 MB | |||
| zignodamus | ✋ | 0 ms | 4.0 MB | |||
| nanoclo | ✋ | 1 ms | 49.4 MB | |||
| nanobruijn | ✋ | 1 ms | 3.3 MB | |||
| kiota | ✋ | 1 ms | 6.6 MB | |||
| official | ✋ | 28 ms | 63.2 MB | |||
| vow-lean-kernel | 🚫 | 83 ms | 8.2 MB | |||
| rpylean | ✋ | 1 ms | 8.0 MB | |||
| official-v4.28.0 | ✋ | 34 ms | 73.6 MB | |||
| still-nanoda | 👍 | 0 ms | 3.0 MB | |||
| nyaya | ✋ | 2 ms | 9.2 MB | |||
| parse-only | 👍 | 27 ms | 60.2 MB |