We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 71efef8 commit 4a0da55Copy full SHA for 4a0da55
src/Data/Nat/Properties.agda
@@ -845,19 +845,6 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
845
------------------------------------------------------------------------
846
-- Bundles
847
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
861
*-magma : Magma 0ℓ 0ℓ
862
*-magma = record
863
{ isMagma = *-isMagma
0 commit comments