Test "tutorial/057_indNegReducible"
Expected: ✋ reject · Size: 1.9 KB · Lines: 31 · lean4export: 3.1.0 · Lean: 4.34.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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | ✋ | 1 ms | 36.0 MB | |||
| mathgraph | ✋ | 1 ms | 29.8 MB | |||
| nanoclo | ✋ | 1 ms | 37.6 MB | |||
| con-ron | ✋ | 1 ms | 11.8 MB | |||
| nanobruijn | ✋ | 0 ms | 3.6 MB | |||
| nanoda | ✋ | 0 ms | 3.1 MB | |||
| lazylean | ✋ | 1 ms | 21.5 MB | |||
| con-leche | ✋ | 3 ms | 19.4 MB | |||
| eink0rn | ✋ | 1 ms | 12.3 MB | |||
| official | ✋ | 28 ms | 67.0 MB | |||
| ind-models | ✋ | 100 ms | 104.2 MB | |||
| lean4lean | ✋ | 28 ms | 95.8 MB | |||
| tenet | ✋ | 118 ms | 44.3 MB | |||
| tenet-hs | ✋ | 1 ms | 8.4 MB | |||
| lean4cobol | ✋ | 2 ms | 13.6 MB | |||
| evmlean | ✋ | 1.1 s | 275.4 MB | |||
| mini | ✋ | 34 ms | 72.8 MB | |||
| overfull | ✋ | 3.4 s | 46.0 MB | |||
| metalean-slow | ✋ | 30 ms | 71.2 MB | |||
| tenet-jvm | ✋ | 101 ms | 64.3 MB | |||
| nanoclo-fortran | ✋ | 1 ms | 4.2 MB | |||
| kiota | ✋ | 1 ms | 6.9 MB | |||
| metalean-fast | ✋ | 30 ms | 71.8 MB | |||
| canonical-min | 🚫 | 387 ms | 1.1 GB | |||
| rpylean | ✋ | 0 ms | 4.3 MB | |||
| vow-lean-kernel | ✋ | 58 ms | 8.4 MB | |||
| parse-only | 👍 | 27 ms | 65.7 MB |