Commit 2022-08-24 11:42 2629553c
View on Github →feat: port 'section relation' in Init/Logic (#379)
#34 left section relation
as a TODO. This PR fills it in.
Compare to the Lean 3 version: https://github.com/leanprover-community/lean/blob/741670c439f1ca266bc7fe61ef7212cc9afd9dd8/library/init/logic.lean#L1027-L1062