Commit 2026-04-29 01:17 89a8a997

View on Github →

feat(Logic/Function/Defs): generalize bicomp to Sort* (#38610) Like Function.comp and Function.onFun, these are general combinators that can work with Sort*.

Estimated changes

Modified Mathlib/Logic/Function/Defs.lean

modified theorem Function.uncurry_bicompl

modified theorem Function.uncurry_bicompr