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

-- 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