@mevenlennonbertrand@lipn.info
Post #2142733
2026-04-22 16:15 UTC
Another day in "having a reliable aka complete kernel is pretty nice", from @BeLazy: fixing incompleteness issues with η for unit fixes open issues with pattern-matching compilation!? (PR: https://github.com/leanprover/lean4/pull/12636)
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-22 16:17
@mevenlennonbertrand@lipn.info Wow, nice! @BeLazy@types.pl