chore: remove useless lines

leanprover · Jan 10, 2025 · c0a5e5b · c0a5e5b
1 parent 4870cb1
commit c0a5e5b
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 3 deletions.
diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean
@@ -29,10 +29,8 @@ structure PlainDateTime where
   The `Time` component of a `PlainTime`
   -/
   time : PlainTime
-
   deriving Inhabited, BEq, Repr
 
-
 namespace PlainDateTime
 
 /--

diff --git a/tests/lean/run/timeLocalDateTime.lean b/tests/lean/run/timeLocalDateTime.lean
@@ -6,7 +6,6 @@ def ShortDateTime : GenericFormat .any := datespec("dd/MM/uuuu HH:mm:ss")
 def ShortDate : GenericFormat .any := datespec("dd/MM/uuuu")
 
 def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.hour PlainDate.minute PlainDate.time.second
-
 def format₂ (PlainDate : PlainDate) : String := ShortDate.formatBuilder PlainDate.day PlainDate.month PlainDate.year
 
 def date₁ := datetime("1993-11-19T09:08:07")