Skip to content

Commit f0c53d6

Browse files
Temporarily remove new GCD definition for v1.5 release (#1400)
1 parent 85cdb08 commit f0c53d6

File tree

3 files changed

+0
-41
lines changed

3 files changed

+0
-41
lines changed

CHANGELOG.md

-1
Original file line numberDiff line numberDiff line change
@@ -199,7 +199,6 @@ New modules
199199
Algebra.Properties.Semiring.Divisibility
200200
Algebra.Properties.Semiring.Exp
201201
Algebra.Properties.Semiring.Exp.TCOptimised
202-
Algebra.Properties.Semiring.GCD
203202
Algebra.Properties.Semiring.Mult
204203
Algebra.Properties.Semiring.Mult.TCOptimised
205204

src/Algebra/Definitions/RawSemiring.agda

-10
Original file line numberDiff line numberDiff line change
@@ -72,13 +72,3 @@ record Prime (p : A) : Set (a ⊔ ℓ) where
7272
p≉0 : p ≉ 0#
7373
split-∣ : {x y} p ∣ x * y p ∣ x ⊎ p ∣ y
7474

75-
------------------------------------------------------------------------
76-
-- Greatest common divisor
77-
78-
record IsGCD (x y gcd : A) : Set (a ⊔ ℓ) where
79-
constructor gcdᶜ
80-
field
81-
divides₁ : gcd ∣ x
82-
divides₂ : gcd ∣ y
83-
greatest : {z} z ∣ x z ∣ y z ∣ gcd
84-

src/Algebra/Properties/Semiring/GCD.agda

-30
This file was deleted.

0 commit comments

Comments
 (0)