{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE EmptyCase                 #-}
{-# LANGUAGE EmptyDataDecls            #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE PatternSynonyms           #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE ScopedTypeVariables       #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Data.Float.Properties where

import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Equality qualified
import MAlonzo.Code.Agda.Builtin.Float qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Data.Maybe.Base qualified
import MAlonzo.Code.Data.Maybe.Properties qualified
import MAlonzo.Code.Data.Nat.Properties qualified
import MAlonzo.Code.Relation.Binary.Bundles qualified
import MAlonzo.Code.Relation.Binary.Construct.On qualified
import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
import MAlonzo.Code.Relation.Binary.Structures qualified
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- Data.Float.Properties.≈⇒≡
d_'8776''8658''8801'_6 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''8658''8801'_6 :: T_Float_6 -> T_Float_6 -> T__'8801'__12 -> T__'8801'__12
d_'8776''8658''8801'_6 = T_Float_6 -> T_Float_6 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Float.Properties.≈-reflexive
d_'8776''45'reflexive_10 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'reflexive_10 :: T_Float_6 -> T_Float_6 -> T__'8801'__12 -> T__'8801'__12
d_'8776''45'reflexive_10 = T_Float_6 -> T_Float_6 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Float.Properties.≈-refl
d_'8776''45'refl_14 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'refl_14 :: T_Float_6 -> T__'8801'__12
d_'8776''45'refl_14 = T_Float_6 -> T__'8801'__12
forall a. a
erased
-- Data.Float.Properties.≈-sym
d_'8776''45'sym_16 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'sym_16 :: T_Float_6 -> T_Float_6 -> T__'8801'__12 -> T__'8801'__12
d_'8776''45'sym_16 = T_Float_6 -> T_Float_6 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Float.Properties.≈-trans
d_'8776''45'trans_18 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'trans_18 :: T_Float_6
-> T_Float_6
-> T_Float_6
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_'8776''45'trans_18 = T_Float_6
-> T_Float_6
-> T_Float_6
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Float.Properties.≈-subst
d_'8776''45'subst_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (MAlonzo.Code.Agda.Builtin.Float.T_Float_6 -> ()) ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> AgdaAny
d_'8776''45'subst_22 :: T_Level_18
-> (T_Float_6 -> T_Level_18)
-> T_Float_6
-> T_Float_6
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
d_'8776''45'subst_22 ~T_Level_18
v0 ~T_Float_6 -> T_Level_18
v1 ~T_Float_6
v2 ~T_Float_6
v3 ~T__'8801'__12
v4 AgdaAny
v5
  = AgdaAny -> AgdaAny
du_'8776''45'subst_22 AgdaAny
v5
du_'8776''45'subst_22 :: AgdaAny -> AgdaAny
du_'8776''45'subst_22 :: AgdaAny -> AgdaAny
du_'8776''45'subst_22 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Data.Float.Properties._≈?_
d__'8776''63'__30 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8776''63'__30 :: T_Float_6 -> T_Float_6 -> T_Dec_20
d__'8776''63'__30
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Float_6 -> T_Float_6 -> T_Dec_20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
MAlonzo.Code.Relation.Binary.Construct.On.du_decidable_102
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 ->
            ((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny)
-> (Word64 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_map_64 Word64 -> Integer
word64ToNat
              ((T_Float_6 -> Maybe Word64) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Float_6 -> Maybe Word64
MAlonzo.Code.Agda.Builtin.Float.d_primFloatToWord64_22 AgdaAny
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20
MAlonzo.Code.Data.Maybe.Properties.du_'8801''45'dec_24
         ((Integer -> Integer -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688))
-- Data.Float.Properties.≈-isEquivalence
d_'8776''45'isEquivalence_32 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_'8776''45'isEquivalence_32 :: T_IsEquivalence_26
d_'8776''45'isEquivalence_32
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Data.Float.Properties.≈-setoid
d_'8776''45'setoid_46 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8776''45'setoid_46 :: T_Setoid_44
d_'8776''45'setoid_46
  = (T_IsEquivalence_26 -> T_Setoid_44)
-> T_IsEquivalence_26 -> T_Setoid_44
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_733
      T_IsEquivalence_26
d_'8776''45'isEquivalence_32
-- Data.Float.Properties.≈-isDecEquivalence
d_'8776''45'isDecEquivalence_48 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_48 :: T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_48
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_20) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3083
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
d_'8776''45'isEquivalence_32) ((T_Float_6 -> T_Float_6 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_Float_6 -> T_Float_6 -> T_Dec_20
d__'8776''63'__30)
-- Data.Float.Properties.≈-decSetoid
d_'8776''45'decSetoid_50 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8776''45'decSetoid_50 :: T_DecSetoid_84
d_'8776''45'decSetoid_50
  = (T_IsDecEquivalence_44 -> T_DecSetoid_84)
-> T_IsDecEquivalence_44 -> T_DecSetoid_84
forall a b. a -> b
coe
      T_IsDecEquivalence_44 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.C_DecSetoid'46'constructor_1389
      T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_48
-- Data.Float.Properties._≟_
d__'8799'__52 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__52 :: T_Float_6 -> T_Float_6 -> T_Dec_20
d__'8799'__52 T_Float_6
v0 T_Float_6
v1
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((T_Float_6 -> T_Float_6 -> T_Dec_20)
-> T_Float_6 -> T_Float_6 -> AgdaAny
forall a b. a -> b
coe T_Float_6 -> T_Float_6 -> T_Dec_20
d__'8776''63'__30 T_Float_6
v0 T_Float_6
v1)
-- Data.Float.Properties.≡-setoid
d_'8801''45'setoid_58 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8801''45'setoid_58 :: T_Setoid_44
d_'8801''45'setoid_58
  = T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe
      T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402
-- Data.Float.Properties.≡-decSetoid
d_'8801''45'decSetoid_60 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8801''45'decSetoid_60 :: T_DecSetoid_84
d_'8801''45'decSetoid_60
  = ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_84)
-> AgdaAny -> T_DecSetoid_84
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
      ((T_Float_6 -> T_Float_6 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_Float_6 -> T_Float_6 -> T_Dec_20
d__'8799'__52)
-- Data.Float.Properties.toWord-injective
d_toWord'45'injective_62 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_toWord'45'injective_62 :: T_Float_6 -> T_Float_6 -> T__'8801'__12 -> T__'8801'__12
d_toWord'45'injective_62 = T_Float_6 -> T_Float_6 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased