------------------------------------------------------------------------ -- The Agda standard library -- -- Properties related to multiplication of integers -- -- This module is DEPRECATED. Please use the corresponding properties in -- Data.Integer.Properties directly. ------------------------------------------------------------------------ module Data.Integer.Multiplication.Properties where open import Data.Integer.Properties public using () renaming ( *-comm to comm ; *-identityˡ to identityˡ ; *-assoc to assoc ; *-isSemigroup to isSemigroup ; *-1-isCommutativeMonoid to isCommutativeMonoid ; *-1-commutativeMonoid to commutativeMonoid )