(* Copyright 2021-2024 Sebastian Lederer. See the file LICENSE.md for details *) function encodefloat32(r:real):integer; external;