------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiates the ring solver with two copies of the same ring with
-- decidable equality
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Solver.Ring.AlmostCommutativeRing using
(AlmostCommutativeRing; -raw-almostCommutative⟶)
open import Relation.Binary.Definitions using (Decidable)
module Algebra.Solver.Ring.Simple
{r₁ r₂} (R : AlmostCommutativeRing r₁ r₂)
(_≟_ : Decidable (AlmostCommutativeRing._≈_ R))
where
open import Relation.Binary.Consequences using (dec⇒weaklyDec)
open AlmostCommutativeRing R
import Algebra.Solver.Ring as RS
open RS rawRing R (-raw-almostCommutative⟶ R) (dec⇒weaklyDec _≟_) public
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4