------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED.
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Operations.Ring
  {ℓ₁ ℓ₂} (ring : RawRing ℓ₁ ℓ₂)
  where

{-# WARNING_ON_IMPORT
"Algebra.Operations.Ring was deprecated in v1.5.
Use Algebra.Properties.Semiring.Exp(.TCOptimised) instead."
#-}

open import Data.Nat.Base as  using (; suc; zero)

open RawRing ring

infixr 8 _^_+1
_^_+1 : Carrier    Carrier
x ^ zero  +1 = x
x ^ suc n +1 = (x ^ n +1) * x

infixr 8 _^_
_^_ : Carrier    Carrier
x ^ zero  = 1#
x ^ suc i = x ^ i +1
{-# INLINE _^_ #-}