------------------------------------------------------------------------
-- The Agda standard library
--
-- Solver for equations in idempotent commutative monoids
--
-- Adapted from Algebra.Solver.CommutativeMonoid
------------------------------------------------------------------------

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

open import Algebra.Bundles using (IdempotentCommutativeMonoid)

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

import Algebra.Solver.IdempotentCommutativeMonoid.Normal as Normal
import Algebra.Solver.Monoid.Solver as Solver

open IdempotentCommutativeMonoid M using (monoid)

private
  module N = Normal M


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

open N public
  renaming (correct to normalise-correct)

------------------------------------------------------------------------
-- Proof procedures

open Solver monoid (record { N }) public


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

-- Version 2.2

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