more operations;
authorwenzelm
Mon, 20 Mar 2023 11:13:01 +0100
changeset 77694 ea509b0bfc80
parent 77693 068ff989c143
child 77695 93531ba2c784
child 77930 84a09beb682d
more operations;
src/Pure/General/space.scala
--- a/src/Pure/General/space.scala	Mon Mar 20 11:09:51 2023 +0100
+++ b/src/Pure/General/space.scala	Mon Mar 20 11:13:01 2023 +0100
@@ -31,6 +31,7 @@
   def + (other: Space): Space = new Space(bytes + other.bytes)
   def - (other: Space): Space = new Space(bytes - other.bytes)
   def * (scalar: Double): Space = new Space((bytes * scalar).round)
+  def / (other: Space): Double = B / other.B
 
   def is_proper: Boolean = bytes > 0
   def is_relevant: Boolean = MiB >= 1.0