Commit 2022-08-31 15:26 90004fda

View on Github →

chore: update 'section binary' in Init/Logic to use infix notation and calc (#386) This makes the code more closely match the mathlib3 version: https://github.com/leanprover-community/lean/blob/741670c439f1ca266bc7fe61ef7212cc9afd9dd8/library/init/logic.lean#L1064-L1097

Estimated changes

modified def RightInverse
modified def associative
modified def commutative
modified def left_cancelative
modified def left_distributive
modified def left_identity
modified def right_cancelative
modified def right_distributive
modified def right_identity