Represents an exact point in time as a UNIX Epoch timestamp.
- val : Duration
Duration since the unix epoch.
Instances For
Equations
- Std.Time.instReprTimestamp = { reprPrec := Std.Time.reprTimestamp✝ }
Equations
- Std.Time.instBEqTimestamp = { beq := Std.Time.beqTimestamp✝ }
Equations
- Std.Time.instInhabitedTimestamp = { default := { val := default } }
Equations
- Std.Time.instLETimestamp = { le := fun (x y : Std.Time.Timestamp) => x.val ≤ y.val }
Equations
- Std.Time.instOfNatTimestamp = { ofNat := { val := OfNat.ofNat n } }
Equations
- Std.Time.instToStringTimestamp = { toString := fun (s : Std.Time.Timestamp) => toString s.val.toSeconds }
@[extern lean_get_current_time]
Fetches the current duration from the system.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- Std.Time.Timestamp.instHSubDuration_1 = { hSub := fun (x y : Std.Time.Timestamp) => x.val - y.val }