    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- A solver for equations over monoids
    ------------------------------------------------------------------------

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

    open import Algebra.Bundles using (Monoid)

    module Algebra.Solver.Monoid {c ℓ} (M : Monoid c ℓ) where

    import Algebra.Solver.Monoid.Normal as Normal
    import Algebra.Solver.Monoid.Solver as Solver
    open import Data.Maybe.Base as Maybe
      using (From-just; from-just)
    open import Data.Product.Base using (_×_; uncurry)
    open import Function.Base using (_∘_)

    private
      module N = Normal M

    ------------------------------------------------------------------------
    -- Normal forms

    open N public
      renaming (comp-correct to homomorphic; correct to normalise-correct)

    ------------------------------------------------------------------------
    -- Tactic

    open Solver M (record { N }) public
      hiding (prove)

    prove : ∀ n (es : Expr n × Expr n) → From-just (uncurry prove′ es)
    prove _ = from-just ∘ uncurry prove′

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.2

    {-# WARNING_ON_USAGE homomorphic
    "Warning: homomorphic was deprecated in v2.2.
    Please use Algebra.Solver.Monoid.Normal.comp-correct instead."
    #-}

    {-# WARNING_ON_USAGE normalise-correct
    "Warning: normalise-correct was deprecated in v2.2.
    Please use Algebra.Solver.Monoid.Normal.correct instead."
    #-}