Test "corner-cases/alg-conv-trans-quot"
Expected: 🤷 either · Size: 8.5 KB · Lines: 169 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source
left composed with right. Quotients of propositions cause
algorithmic conversion transitivity to fail because the typechecker must
creatively synthesise the representative of the quotient, and
proof irrelevance is definitional.
References:
- Mario Carneiro, The Type Theory of Lean, MSc thesis
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | ✋ | 1 ms | 33.8 MB | |||
| nanoda | ✋ | 1 ms | 3.2 MB | |||
| nanobruijn | ✋ | 1 ms | 8.5 MB | |||
| ind-models | ✋ | 60 ms | 105.7 MB | |||
| official | ✋ | 30 ms | 67.3 MB | |||
| lean4lean | ✋ | 74 ms | 105.6 MB | |||
| evmlean | ✋ | 3.1 s | 143.6 MB | |||
| mini | ✋ | 36 ms | 74.8 MB | |||
| sokonanoda | ✋ | 1 ms | 34.0 MB | |||
| nanoclo | ✋ | 1 ms | 41.3 MB | |||
| zignodamus | ✋ | 1 ms | 5.0 MB | |||
| vow-lean-kernel | ✋ | 77 ms | 8.4 MB | |||
| official-v4.28.0 | ✋ | 37 ms | 74.5 MB | |||
| still-nanoda | ✋ | 1 ms | 3.2 MB | |||
| kiota | ✋ | 1 ms | 9.2 MB | |||
| rpylean | ✋ | 1 ms | 8.9 MB | |||
| nyaya | ✋ | 3 ms | 10.3 MB | |||
| parse-only | 👍 | 28 ms | 65.6 MB |