.

leanprover · Dec 19, 2024 · 1890704 · 1890704
1 parent 75772e3
commit 1890704
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/src/Init/Data/Range/Basic.lean b/src/Init/Data/Range/Basic.lean
@@ -23,11 +23,7 @@ namespace Range
 universe u v
 
 /-- The number of elements in the range. -/
-<<<<<<< HEAD
 @[simp] def size (r : Range) : Nat := (r.stop - r.start + r.step - 1) / r.step
-=======
-def size (r : Range) : Nat := (r.stop - r.start + r.step - 1) / r.step
->>>>>>> origin/master
 
 @[inline] protected def forIn' [Monad m] (range : Range) (init : β)
     (f : (i : Nat) → i ∈ range → β → m (ForInStep β)) : m β :=