Source code on Github
{-# OPTIONS --cubical-compatible --safe --no-sized-types --no-guardedness #-}

module Agda.Builtin.Float.Properties where

open import Agda.Builtin.Float
open import Agda.Builtin.Equality

primitive

  primFloatToWord64Injective :  a b  primFloatToWord64 a  primFloatToWord64 b  a  b