    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- This module collects the property definitions for left-scaling
    -- (LeftDefs), right-scaling (RightDefs), and both (BiDefs).
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Algebra.Module.Definitions where

      import Algebra.Module.Definitions.Left as L
      import Algebra.Module.Definitions.Right as R
      import Algebra.Module.Definitions.Bi as B
      import Algebra.Module.Definitions.Bi.Simultaneous as BS

      module LeftDefs = L
      module RightDefs = R
      module BiDefs = B
      module SimultaneousBiDefs = BS