# Write a floating point `value` on 64 bits
	fun write_double(value: Float)
	do
		for i in [0..8[ do write_byte value.double_byte_at(i, big_endian)
	end