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

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary

module Algebra.Module.Definitions where

  open import Algebra.Core

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

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