{-# 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.Relation.Binary.Structures.Biased 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.Primitive
import qualified MAlonzo.Code.Relation.Binary.Consequences
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Relation.Binary.Structures.Biased._.IsEquivalence
d_IsEquivalence_30 :: p -> p -> p -> p -> ()
d_IsEquivalence_30 p
a0 p
a1 p
a2 p
a3 = ()
-- Relation.Binary.Structures.Biased._.IsStrictTotalOrder
d_IsStrictTotalOrder_40 :: p -> p -> p -> p -> p -> p -> ()
d_IsStrictTotalOrder_40 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Structures.Biased._.IsEquivalence.refl
d_refl_274 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  AgdaAny -> AgdaAny
d_refl_274 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny
d_refl_274 T_IsEquivalence_26
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)
-- Relation.Binary.Structures.Biased._.IsEquivalence.sym
d_sym_278 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_278 :: T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_278 T_IsEquivalence_26
v0
  = (T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)
-- Relation.Binary.Structures.Biased._.IsEquivalence.trans
d_trans_280 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_280 :: T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_280 T_IsEquivalence_26
v0
  = (T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0)
-- Relation.Binary.Structures.Biased._.IsStrictTotalOrder.compare
d_compare_402 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
d_compare_402 :: T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
d_compare_402 T_IsStrictTotalOrder_534
v0
  = (T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tri_158
forall a b. a -> b
coe
      T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_544 (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
v0)
-- Relation.Binary.Structures.Biased._.IsStrictTotalOrder.isStrictPartialOrder
d_isStrictPartialOrder_412 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
d_isStrictPartialOrder_412 :: T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290
d_isStrictPartialOrder_412 T_IsStrictTotalOrder_534
v0
  = (T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> T_IsStrictPartialOrder_290
forall a b. a -> b
coe
      T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_542
      (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
v0)
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ
d_IsStrictTotalOrder'7580'_522 :: p -> p -> p -> p -> p -> p -> ()
d_IsStrictTotalOrder'7580'_522 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsStrictTotalOrder'7580'_522
  = C_IsStrictTotalOrder'7580''46'constructor_6029 MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
                                                   (AgdaAny ->
                                                    AgdaAny ->
                                                    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                                   (AgdaAny ->
                                                    AgdaAny ->
                                                    MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158)
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ.isEquivalence
d_isEquivalence_532 ::
  T_IsStrictTotalOrder'7580'_522 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_532 :: T_IsStrictTotalOrder'7580'_522 -> T_IsEquivalence_26
d_isEquivalence_532 T_IsStrictTotalOrder'7580'_522
v0
  = case T_IsStrictTotalOrder'7580'_522 -> T_IsStrictTotalOrder'7580'_522
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_522
v0 of
      C_IsStrictTotalOrder'7580''46'constructor_6029 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> T_Tri_158
v3 -> T_IsEquivalence_26 -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsEquivalence_26
v1
      T_IsStrictTotalOrder'7580'_522
_ -> T_IsEquivalence_26
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ.trans
d_trans_534 ::
  T_IsStrictTotalOrder'7580'_522 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_534 :: T_IsStrictTotalOrder'7580'_522
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_534 T_IsStrictTotalOrder'7580'_522
v0
  = case T_IsStrictTotalOrder'7580'_522 -> T_IsStrictTotalOrder'7580'_522
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_522
v0 of
      C_IsStrictTotalOrder'7580''46'constructor_6029 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> T_Tri_158
v3 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_IsStrictTotalOrder'7580'_522
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ.compare
d_compare_536 ::
  T_IsStrictTotalOrder'7580'_522 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
d_compare_536 :: T_IsStrictTotalOrder'7580'_522 -> AgdaAny -> AgdaAny -> T_Tri_158
d_compare_536 T_IsStrictTotalOrder'7580'_522
v0
  = case T_IsStrictTotalOrder'7580'_522 -> T_IsStrictTotalOrder'7580'_522
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_522
v0 of
      C_IsStrictTotalOrder'7580''46'constructor_6029 T_IsEquivalence_26
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> T_Tri_158
v3 -> (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_158
v3
      T_IsStrictTotalOrder'7580'_522
_ -> AgdaAny -> AgdaAny -> T_Tri_158
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ.isStrictTotalOrderᶜ
d_isStrictTotalOrder'7580'_538 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_IsStrictTotalOrder'7580'_522 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
d_isStrictTotalOrder'7580'_538 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictTotalOrder'7580'_522
-> T_IsStrictTotalOrder_534
d_isStrictTotalOrder'7580'_538 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsStrictTotalOrder'7580'_522
v6
  = T_IsStrictTotalOrder'7580'_522 -> T_IsStrictTotalOrder_534
du_isStrictTotalOrder'7580'_538 T_IsStrictTotalOrder'7580'_522
v6
du_isStrictTotalOrder'7580'_538 ::
  T_IsStrictTotalOrder'7580'_522 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
du_isStrictTotalOrder'7580'_538 :: T_IsStrictTotalOrder'7580'_522 -> T_IsStrictTotalOrder_534
du_isStrictTotalOrder'7580'_538 T_IsStrictTotalOrder'7580'_522
v0
  = (T_IsStrictPartialOrder_290
 -> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_534)
-> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_534
forall a b. a -> b
coe
      T_IsStrictPartialOrder_290
-> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_24953
      ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_290)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_14045
         (T_IsStrictTotalOrder'7580'_522 -> T_IsEquivalence_26
d_isEquivalence_532 (T_IsStrictTotalOrder'7580'_522 -> T_IsStrictTotalOrder'7580'_522
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_522
v0)) (T_IsStrictTotalOrder'7580'_522
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_534 (T_IsStrictTotalOrder'7580'_522 -> T_IsStrictTotalOrder'7580'_522
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_522
v0))
         (((AgdaAny -> AgdaAny -> T_Tri_158) -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> T_Tri_158) -> T_Σ_14
MAlonzo.Code.Relation.Binary.Consequences.du_trans'8743'tri'8658'resp_716
            ((T_IsStrictTotalOrder'7580'_522 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_522 -> AgdaAny -> AgdaAny -> T_Tri_158
d_compare_536 (T_IsStrictTotalOrder'7580'_522 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_522
v0))))
      ((T_IsStrictTotalOrder'7580'_522 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_522 -> AgdaAny -> AgdaAny -> T_Tri_158
d_compare_536 (T_IsStrictTotalOrder'7580'_522 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_522
v0))