{-# 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.Unit.Properties where

import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Bool qualified
import MAlonzo.Code.Agda.Builtin.Equality qualified
import MAlonzo.Code.Agda.Builtin.Unit qualified
import MAlonzo.Code.Data.Sum.Base qualified
import MAlonzo.Code.Relation.Binary.Bundles 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.Code.Relation.Nullary.Reflects 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.Unit.Properties.⊤-irrelevant
d_'8868''45'irrelevant_6 ::
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8868''45'irrelevant_6 :: T_'8868'_6 -> T_'8868'_6 -> T__'8801'__12
d_'8868''45'irrelevant_6 = T_'8868'_6 -> T_'8868'_6 -> T__'8801'__12
forall a. a
erased
-- Data.Unit.Properties._≟_
d__'8799'__8 ::
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__8 :: T_'8868'_6 -> T_'8868'_6 -> T_Dec_20
d__'8799'__8 ~T_'8868'_6
v0 ~T_'8868'_6
v1 = T_Dec_20
du__'8799'__8
du__'8799'__8 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du__'8799'__8 :: T_Dec_20
du__'8799'__8
  = (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
      Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
      (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
      ((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
forall a. a
erased)
-- Data.Unit.Properties.≡-setoid
d_'8801''45'setoid_10 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8801''45'setoid_10 :: T_Setoid_44
d_'8801''45'setoid_10
  = 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.Unit.Properties.≡-decSetoid
d_'8801''45'decSetoid_12 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8801''45'decSetoid_12 :: T_DecSetoid_84
d_'8801''45'decSetoid_12
  = ((Any -> Any -> T_Dec_20) -> T_DecSetoid_84)
-> (Any -> Any -> Any) -> T_DecSetoid_84
forall a b. a -> b
coe
      (Any -> Any -> T_Dec_20) -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
      (\ Any
v0 Any
v1 -> T_Dec_20 -> Any
forall a b. a -> b
coe T_Dec_20
du__'8799'__8)
-- Data.Unit.Properties.≡-total
d_'8801''45'total_14 ::
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8801''45'total_14 :: T_'8868'_6 -> T_'8868'_6 -> T__'8846'__30
d_'8801''45'total_14 ~T_'8868'_6
v0 ~T_'8868'_6
v1 = T__'8846'__30
du_'8801''45'total_14
du_'8801''45'total_14 :: MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8801''45'total_14 :: T__'8846'__30
du_'8801''45'total_14
  = (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
forall a. a
erased
-- Data.Unit.Properties.≡-antisym
d_'8801''45'antisym_16 ::
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_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_'8801''45'antisym_16 :: T_'8868'_6
-> T_'8868'_6 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12
d_'8801''45'antisym_16 = T_'8868'_6
-> T_'8868'_6 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Data.Unit.Properties.≡-isPreorder
d_'8801''45'isPreorder_20 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8801''45'isPreorder_20 :: T_IsPreorder_70
d_'8801''45'isPreorder_20
  = (T_IsEquivalence_26
 -> (Any -> Any -> Any -> Any)
 -> (Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsPreorder_70)
-> Any -> Any -> Any -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
      (T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2)) Any
forall a. a
erased
-- Data.Unit.Properties.≡-isPartialOrder
d_'8801''45'isPartialOrder_24 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_'8801''45'isPartialOrder_24 :: T_IsPartialOrder_174
d_'8801''45'isPartialOrder_24
  = (T_IsPreorder_70
 -> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_174)
-> Any -> Any -> T_IsPartialOrder_174
forall a b. a -> b
coe
      T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
      (T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8801''45'isPreorder_20) Any
forall a. a
erased
-- Data.Unit.Properties.≡-isTotalOrder
d_'8801''45'isTotalOrder_26 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_404
d_'8801''45'isTotalOrder_26 :: T_IsTotalOrder_404
d_'8801''45'isTotalOrder_26
  = (T_IsPartialOrder_174
 -> (Any -> Any -> T__'8846'__30) -> T_IsTotalOrder_404)
-> Any -> (Any -> Any -> Any) -> T_IsTotalOrder_404
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> (Any -> Any -> T__'8846'__30) -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_20555
      (T_IsPartialOrder_174 -> Any
forall a b. a -> b
coe T_IsPartialOrder_174
d_'8801''45'isPartialOrder_24)
      (\ Any
v0 Any
v1 -> T__'8846'__30 -> Any
forall a b. a -> b
coe T__'8846'__30
du_'8801''45'total_14)
-- Data.Unit.Properties.≡-isDecTotalOrder
d_'8801''45'isDecTotalOrder_28 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460
d_'8801''45'isDecTotalOrder_28 :: T_IsDecTotalOrder_460
d_'8801''45'isDecTotalOrder_28
  = (T_IsTotalOrder_404
 -> (Any -> Any -> T_Dec_20)
 -> (Any -> Any -> T_Dec_20)
 -> T_IsDecTotalOrder_460)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> T_IsDecTotalOrder_460
forall a b. a -> b
coe
      T_IsTotalOrder_404
-> (Any -> Any -> T_Dec_20)
-> (Any -> Any -> T_Dec_20)
-> T_IsDecTotalOrder_460
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_22695
      (T_IsTotalOrder_404 -> Any
forall a b. a -> b
coe T_IsTotalOrder_404
d_'8801''45'isTotalOrder_26) (\ Any
v0 Any
v1 -> T_Dec_20 -> Any
forall a b. a -> b
coe T_Dec_20
du__'8799'__8)
      (\ Any
v0 Any
v1 -> T_Dec_20 -> Any
forall a b. a -> b
coe T_Dec_20
du__'8799'__8)
-- Data.Unit.Properties.≡-poset
d_'8801''45'poset_30 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_'8801''45'poset_30 :: T_Poset_314
d_'8801''45'poset_30
  = (T_IsPartialOrder_174 -> T_Poset_314)
-> T_IsPartialOrder_174 -> T_Poset_314
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
      T_IsPartialOrder_174
d_'8801''45'isPartialOrder_24
-- Data.Unit.Properties.≡-decTotalOrder
d_'8801''45'decTotalOrder_32 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_866
d_'8801''45'decTotalOrder_32 :: T_DecTotalOrder_866
d_'8801''45'decTotalOrder_32
  = (T_IsDecTotalOrder_460 -> T_DecTotalOrder_866)
-> T_IsDecTotalOrder_460 -> T_DecTotalOrder_866
forall a b. a -> b
coe
      T_IsDecTotalOrder_460 -> T_DecTotalOrder_866
MAlonzo.Code.Relation.Binary.Bundles.C_DecTotalOrder'46'constructor_17849
      T_IsDecTotalOrder_460
d_'8801''45'isDecTotalOrder_28