Concern with `instance OfNat Timestamp` (and `Duration`)

Stream: lean4

[Chris Wong]

Hi all,

I've been looking at the new time library and it looks really good!

I have a minor concern about docs#Std.Time.instOfNatTimestamp and docs#Std.Time.instOfNatDuration. Those instances assume seconds. However, JavaScript uses milliseconds. If a developer blindly copies a value from their JavaScript code to Lean, they'll end up with a duration that's off by a factor of 1000.

Have we considered removing these two instances? We can use instead Timestamp.ofSecondsSinceUnixEpoch which is safer.

[Eric Wieser]

Or even have custom 10s / 10ms notation

[Markus Himmel]

Yes, let's track this at lean4#6793.