Skip to content

Commit 4a0da55

Browse files
committed
removed duplicate bundle from
1 parent 71efef8 commit 4a0da55

File tree

1 file changed

+0
-13
lines changed

1 file changed

+0
-13
lines changed

src/Data/Nat/Properties.agda

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -845,19 +845,6 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
845845
------------------------------------------------------------------------
846846
-- Bundles
847847

848-
*-rawMagma : RawMagma 0ℓ 0ℓ
849-
*-rawMagma = record
850-
{ _≈_ = _≡_
851-
; _∙_ = _*_
852-
}
853-
854-
*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
855-
*-1-rawMonoid = record
856-
{ _≈_ = _≡_
857-
; _∙_ = _*_
858-
; ε = 1
859-
}
860-
861848
*-magma : Magma 0ℓ 0ℓ
862849
*-magma = record
863850
{ isMagma = *-isMagma

0 commit comments

Comments
 (0)