{-# 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.Word.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.Primitive
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
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Data.Word.Properties.≈⇒≡
d_'8776''8658''8801'_6 ::
  MAlonzo.RTE.Word64 ->
  MAlonzo.RTE.Word64 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''8658''8801'_6 :: Word64 -> Word64 -> T__'8801'__12 -> T__'8801'__12
d_'8776''8658''8801'_6 = Word64 -> Word64 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Word.Properties.≈-reflexive
d_'8776''45'reflexive_8 ::
  MAlonzo.RTE.Word64 ->
  MAlonzo.RTE.Word64 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'reflexive_8 :: Word64 -> Word64 -> T__'8801'__12 -> T__'8801'__12
d_'8776''45'reflexive_8 = Word64 -> Word64 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Word.Properties.≈-refl
d_'8776''45'refl_10 ::
  MAlonzo.RTE.Word64 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'refl_10 :: Word64 -> T__'8801'__12
d_'8776''45'refl_10 = Word64 -> T__'8801'__12
forall a. a
erased
-- Data.Word.Properties.≈-sym
d_'8776''45'sym_12 ::
  MAlonzo.RTE.Word64 ->
  MAlonzo.RTE.Word64 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8776''45'sym_12 :: Word64 -> Word64 -> T__'8801'__12 -> T__'8801'__12
d_'8776''45'sym_12 = Word64 -> Word64 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Word.Properties.≈-trans
d_'8776''45'trans_14 ::
  MAlonzo.RTE.Word64 ->
  MAlonzo.RTE.Word64 ->
  MAlonzo.RTE.Word64 ->
  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_14 :: Word64
-> Word64
-> Word64
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_'8776''45'trans_14 = Word64
-> Word64
-> Word64
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Word.Properties.≈-subst
d_'8776''45'subst_18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (MAlonzo.RTE.Word64 -> ()) ->
  MAlonzo.RTE.Word64 ->
  MAlonzo.RTE.Word64 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny -> AgdaAny
d_'8776''45'subst_18 :: T_Level_18
-> (Word64 -> T_Level_18)
-> Word64
-> Word64
-> T__'8801'__12
-> AgdaAny
-> AgdaAny
d_'8776''45'subst_18 ~T_Level_18
v0 ~Word64 -> T_Level_18
v1 ~Word64
v2 ~Word64
v3 ~T__'8801'__12
v4 AgdaAny
v5
  = AgdaAny -> AgdaAny
du_'8776''45'subst_18 AgdaAny
v5
du_'8776''45'subst_18 :: AgdaAny -> AgdaAny
du_'8776''45'subst_18 :: AgdaAny -> AgdaAny
du_'8776''45'subst_18 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Data.Word.Properties._≈?_
d__'8776''63'__26 ::
  MAlonzo.RTE.Word64 ->
  MAlonzo.RTE.Word64 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8776''63'__26 :: Word64 -> Word64 -> T_Dec_32
d__'8776''63'__26 Word64
v0 Word64
v1
  = (Integer -> Integer -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'8799'__1528
      ((Word64 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Word64 -> Integer
word64ToNat (Word64 -> AgdaAny
forall a b. a -> b
coe Word64
v0)) ((Word64 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Word64 -> Integer
word64ToNat (Word64 -> AgdaAny
forall a b. a -> b
coe Word64
v1))
-- Data.Word.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_743
      AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Data.Word.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_727
      T_IsEquivalence_26
d_'8776''45'isEquivalence_32
-- Data.Word.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_32) -> T_IsDecEquivalence_44)
-> AgdaAny -> AgdaAny -> T_IsDecEquivalence_44
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3075
      (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
d_'8776''45'isEquivalence_32) ((Word64 -> Word64 -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe Word64 -> Word64 -> T_Dec_32
d__'8776''63'__26)
-- Data.Word.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_1385
      T_IsDecEquivalence_44
d_'8776''45'isDecEquivalence_48
-- Data.Word.Properties._≟_
d__'8799'__52 ::
  MAlonzo.RTE.Word64 ->
  MAlonzo.RTE.Word64 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8799'__52 :: Word64 -> Word64 -> T_Dec_32
d__'8799'__52 Word64
v0 Word64
v1
  = ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
      AgdaAny
forall a. a
erased ((Word64 -> Word64 -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Word64 -> Word64 -> T_Dec_32
d__'8776''63'__26 (Word64 -> AgdaAny
forall a b. a -> b
coe Word64
v0) (Word64 -> AgdaAny
forall a b. a -> b
coe Word64
v1))
-- Data.Word.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_250
-- Data.Word.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_32) -> T_DecSetoid_84)
-> AgdaAny -> T_DecSetoid_84
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_254
      ((Word64 -> Word64 -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe Word64 -> Word64 -> T_Dec_32
d__'8799'__52)
-- Data.Word.Properties._==_
d__'61''61'__62 :: MAlonzo.RTE.Word64 -> MAlonzo.RTE.Word64 -> Bool
d__'61''61'__62 :: Word64 -> Word64 -> Bool
d__'61''61'__62 Word64
v0 Word64
v1
  = (T_Level_18 -> T_Level_18 -> T_Dec_32 -> Bool)
-> T_Level_18 -> AgdaAny -> T_Dec_32 -> Bool
forall a b. a -> b
coe
      T_Level_18 -> T_Level_18 -> T_Dec_32 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_'8970'_'8971'_22 ()
      AgdaAny
forall a. a
erased (Word64 -> Word64 -> T_Dec_32
d__'8799'__52 (Word64 -> Word64
forall a b. a -> b
coe Word64
v0) (Word64 -> Word64
forall a b. a -> b
coe Word64
v1))
-- Data.Word.Properties._<?_
d__'60''63'__68 ::
  MAlonzo.RTE.Word64 ->
  MAlonzo.RTE.Word64 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'60''63'__68 :: Word64 -> Word64 -> T_Dec_32
d__'60''63'__68
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> Word64 -> Word64 -> T_Dec_32
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
MAlonzo.Code.Relation.Binary.Construct.On.du_decidable_102
      ((Word64 -> Integer) -> AgdaAny
forall a b. a -> b
coe Word64 -> Integer
word64ToNat)
      ((Integer -> Integer -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'60''63'__1912)
-- Data.Word.Properties.<-strictTotalOrder-≈
d_'60''45'strictTotalOrder'45''8776'_70 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
d_'60''45'strictTotalOrder'45''8776'_70 :: T_StrictTotalOrder_864
d_'60''45'strictTotalOrder'45''8776'_70
  = (T_StrictTotalOrder_864
 -> (AgdaAny -> AgdaAny) -> T_StrictTotalOrder_864)
-> AgdaAny -> AgdaAny -> T_StrictTotalOrder_864
forall a b. a -> b
coe
      T_StrictTotalOrder_864
-> (AgdaAny -> AgdaAny) -> T_StrictTotalOrder_864
MAlonzo.Code.Relation.Binary.Construct.On.du_strictTotalOrder_618
      (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe
         T_StrictTotalOrder_864
MAlonzo.Code.Data.Nat.Properties.d_'60''45'strictTotalOrder_1934)
      ((Word64 -> Integer) -> AgdaAny
forall a b. a -> b
coe Word64 -> Integer
word64ToNat)