← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda-stdlib/wily

« back to all changes in this revision

Viewing changes to src/Algebra/RingSolver/Simple.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-05-27 19:29:25 UTC
  • mfrom: (8.1.1 experimental)
  • Revision ID: package-import@ubuntu.com-20130527192925-q2tadfousmn0xeav
Tags: 0.7-2
Upload to unstable 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/RingSolver/Simple.agda
1
1
------------------------------------------------------------------------
2
2
-- The Agda standard library
3
3
--
 
4
-- Instantiates the ring solver with two copies of the same ring with
 
5
-- decidable equality
4
6
------------------------------------------------------------------------
5
7
 
6
8
open import Algebra.RingSolver.AlmostCommutativeRing
 
9
open import Relation.Binary
7
10
 
8
11
module Algebra.RingSolver.Simple
9
12
         {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂)
 
13
         (_≟_ : Decidable (AlmostCommutativeRing._≈_ R))
10
14
         where
11
15
 
12
16
open AlmostCommutativeRing R
13
17
import Algebra.RingSolver as RS
14
 
open RS rawRing R (-raw-almostCommutative⟶ R) public
 
18
open RS rawRing R (-raw-almostCommutative⟶ R) _≟_ public