← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Algebra/RingSolver.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (2.1.4 sid)
  • Revision ID: package-import@ubuntu.com-20111129170035-be8cbok8ojft5tjl
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Algebra/RingSolver.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Solver for commutative ring or semiring equalities
3
5
------------------------------------------------------------------------
4
6
 
5
 
{-# OPTIONS --universe-polymorphism #-}
6
 
 
7
7
-- Uses ideas from the Coq ring tactic. See "Proving Equalities in a
8
8
-- Commutative Ring Done Right in Coq" by Grégoire and Mahboubi. The
9
9
-- code below is not optimised like theirs, though.
34
34
open import Data.Fin as Fin using (Fin; zero; suc)
35
35
open import Data.Vec
36
36
open import Function hiding (type-signature)
37
 
open import Level
 
37
open import Level using (_⊔_)
38
38
 
39
39
infix  9 _↑ :-_ -‿NF_
40
40
infixr 9 _:^_ _^-NF_ _:↑_