Commit 2026-03-21 09:03 d6a98e30

View on Github →

chore(Order/Hom/Lattice): clean up to_dual use (#36609) This PR cleans up the use of to_dual for LatticeHom after #36159, avoiding to_dual existing where this is not needed. Another benefit of this PR is that LatticeHom.toInfHom now becomes reducible, just like LatticeHom.toSupHom, as a result of generating it with extends.

Estimated changes