cartesian): make exp right-associative (#11172)

Commit

4 years ago

chore(category_theory/closed/cartesian): make exp right-associative (#11172) This makes `X ⟹ Y ⟹ Z` parse as `X ⟹ (Y ⟹ Z)`, like ordinary function types.

Author

dwarn

Parents

559951cd

mathlib 8db2fa05 - chore(category_theory/closed/cartesian): make exp right-associative (#11172)

mathlib
8db2fa05 - chore(category_theory/closed/cartesian): make exp right-associative (#11172)