diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index 88b62af53dd4..f6c16e349d11 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -914,9 +914,9 @@ private def dateFromModifier (date : DateTime tz) : TypeFormat modifier := | .H _ => date.hour | .m _ => date.minute | .s _ => date.date.get.time.second - | .S _ => date.nanoseconds + | .S _ => date.nanosecond | .A _ => date.date.get.time.toMilliseconds - | .n _ => date.nanoseconds + | .n _ => date.nanosecond | .N _ => date.date.get.time.toNanoseconds | .V => tz.name | .z .short => tz.abbreviation