Test "tutorial/054_indNegReducible"
Expected: ✋ reject · Size: 1.9 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source
When checking inductives, we expect the kernel to not reduce the type of the constructor parameters further than head normal form. Recursive occurrences nested inside the head normal form are considered negative occurrences, even if they could be reduced to disappear.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| nanoda | ✋ | 1 ms | 2.9 MB | |||
| nanobruijn | ✋ | 2 ms | 3.2 MB | |||
| official-nightly | ✋ | 31 ms | 56.7 MB | |||
| official | ✋ | 31 ms | 67.0 MB | |||
| official-v4.28.0 | ✋ | 37 ms | 71.0 MB | |||
| lean4lean | ✋ | 57 ms | 85.6 MB | |||
| mini | ✋ | 38 ms | 71.0 MB | |||
| vow-lean-kernel | ✋ | 62 ms | 7.8 MB | |||
| evmlean | ✋ | 517 ms | 126.7 MB | |||
| always-decline | 🚫 | 1 ms | 2.9 MB | |||
| sokonanoda | ✋ | 1 ms | 2.9 MB | |||
| rpylean | ✋ | 2 ms | 7.9 MB | |||
| still-nanoda | ✋ | 1 ms | 2.9 MB | |||
| always-reject | ✋ | 1 ms | 2.9 MB | |||
| parse-only | 👍 | 37 ms | 71.1 MB | |||
| always-accept | 👍 | 1 ms | 2.9 MB |