remove algebra

katydid · Aug 23, 2024 · 2e16ec9 · 2e16ec9
1 parent 0538399
commit 2e16ec9
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 180 deletions.
diff --git a/Katydid/Std/Algebra.lean b/Katydid/Std/Algebra.lean
diff --git a/Katydid/Std/AlgebraExamples.lean b/Katydid/Std/AlgebraExamples.lean
diff --git a/Katydid/Std/Ordering.lean b/Katydid/Std/Ordering.lean
@@ -1,5 +1,3 @@
-import Katydid.Std.Algebra
-
 instance : Repr Ordering where
   reprPrec
     | Ordering.lt, _ => "<"
@@ -67,51 +65,3 @@ theorem lex_right_identity'':
   { rfl }
 
 end Ordering
-
-instance : Magma Ordering where
-  op a b := Ordering.lex a b
-
-instance : Semigroup Ordering where
-  is_assoc := Ordering.lex_assoc
-
-instance : Monoid Ordering where
-  id := Ordering.eq
-  left_identity := Ordering.lex_left_identity
-  right_identity := Ordering.lex_right_identity
-
-section instances_using_structure'
-
-  open algebra_using_structure'
-
-  def instanceMagmaLex := Magma'Struct.mk Ordering Ordering.lex
-  def instanceMagmaLex': Magma'Struct := {
-    carrier := Ordering,
-    op := Ordering.lex
-  }
-
-  def instanceSemigroupLex : Semigroup'Struct := {
-    toMagma'Struct := instanceMagmaLex,
-    is_assoc := Ordering.lex_assoc
-  }
-  def instanceSemigroupLex' : Semigroup'Struct := {
-    carrier := Ordering,
-    op := Ordering.lex,
-    is_assoc := Ordering.lex_assoc
-  }
-
-  def instanceMonoidLex : Monoid'Struct := {
-    carrier := Ordering,
-    op := Ordering.lex,
-    is_assoc := Ordering.lex_assoc,
-    e := Ordering.eq,
-    left_identity := Ordering.lex_left_identity,
-    right_identity := Ordering.lex_right_identity,
-  }
-  def instanceMonoidLex' : Monoid'Struct := {
-    toSemigroup'Struct := instanceSemigroupLex,
-    e := Ordering.eq,
-    left_identity := Ordering.lex_left_identity,
-    right_identity := Ordering.lex_right_identity,
-  }
-
-end instances_using_structure'
diff --git a/Katydid/Std/ThunkOrdering.lean b/Katydid/Std/ThunkOrdering.lean
@@ -1,5 +1,3 @@
-import Katydid.Std.Algebra
-
 instance : Repr (Thunk Ordering) where
   reprPrec thunk _ :=
     match thunk.get with
@@ -39,15 +37,3 @@ theorem lex_right_identity (a: Thunk Ordering):
     rfl
 
 end ThunkOrdering
-
-instance : Magma (Thunk Ordering) where
-  op a b := ThunkOrdering.lex a b
-
-instance : Semigroup (Thunk Ordering) where
-  is_assoc := ThunkOrdering.lex_assoc
-
-instance : Monoid (Thunk Ordering) where
-  id := Ordering.eq
-  left_identity := ThunkOrdering.lex_left_identity
-  right_identity := ThunkOrdering.lex_right_identity
-