diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index bbfe331812e1..dd6fc91cc785 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -30,7 +30,8 @@ structure PlainDateTime where -/ time : PlainTime - deriving Repr, Inhabited + deriving Inhabited, BEq, Repr + namespace PlainDateTime