notations for left and right module actions

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory

http://homotopytypetheory.org/

Other

1.26k stars 192 forks source link

Closed Alizter closed 4 months ago

Alizter commented 4 months ago

In this PR we introduce notations r *L m for lact r m and m *R r for ract m r. If we don't like them, then we can drop this PR.