Lean Kernel Arena / logos-kernel / bugs/rec-of-subst-prop

Checker: logos-kernel · Version: 1e6ad5b · 📄 Declaration · 🔗 Source

Test: bugs/rec-of-subst-prop · Expected: ✋ reject · Size: 269.2 KB · Lines: 5.1 k · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source

Result: ✋ rejected · exit code 1 · wall time: 5.29 ms · instructions: 14.2 M · max rss memory: 5.8 MB · run 2026-11-08 11:08:24 UTC

stderr:

rejected: declaration 'Issue.forallFalse': application type mismatch
  in `Issue.identityValue Empty (Issue.Owner.rec Issue.gateWitness (fun (x0 : Issue.proposition) => Issue.Fiber Empty) (Issue.transport Empty) (Issue.delayedOwner #2 (Issue.Owner.mk Issue.gateWitness Empty))) (Issue.identityValue Unit (Issue.Owner.rec Issue.gateWitness (fun (x0 : Issue.proposition) => Issue.Fiber Unit) (Issue.transport Unit) (Issue.delayedOwner #2 (Issue.Owner.mk Issue.gateWitness Unit))) Unit.unit)`
  expected type: Issue.preserveType Empty
  but the argument has type: Issue.preserveType Unit