fun get_double(key: JavaString): Float in "Java" `{ return self.getDouble(key); `}