{-# 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_46 :: p -> p -> p -> p -> ()
d_IsEquivalence_46 p
a0 p
a1 p
a2 p
a3 = ()
-- Relation.Binary.Structures.Biased._.IsStrictTotalOrder
d_IsStrictTotalOrder_66 :: p -> p -> p -> p -> p -> p -> ()
d_IsStrictTotalOrder_66 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Relation.Binary.Structures.Biased._.IsEquivalence.refl
d_refl_356 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  AgdaAny -> AgdaAny
d_refl_356 :: T_IsEquivalence_28 -> AgdaAny -> AgdaAny
d_refl_356 T_IsEquivalence_28
v0
  = (T_IsEquivalence_28 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0)
-- Relation.Binary.Structures.Biased._.IsEquivalence.sym
d_sym_360 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_360 :: T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_sym_360 T_IsEquivalence_28
v0
  = (T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0)
-- Relation.Binary.Structures.Biased._.IsEquivalence.trans
d_trans_362 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_362 :: T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_362 T_IsEquivalence_28
v0
  = (T_IsEquivalence_28
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_40 (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
v0)
-- Relation.Binary.Structures.Biased._.IsStrictTotalOrder.compare
d_compare_484 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
d_compare_484 :: T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158
d_compare_484 T_IsStrictTotalOrder_624
v0
  = (T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tri_158
forall a b. a -> b
coe
      T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_634 (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)
-- Relation.Binary.Structures.Biased._.IsStrictTotalOrder.isStrictPartialOrder
d_isStrictPartialOrder_494 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
d_isStrictPartialOrder_494 :: T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
d_isStrictPartialOrder_494 T_IsStrictTotalOrder_624
v0
  = (T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
      T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
      (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ
d_IsStrictTotalOrder'7580'_604 :: p -> p -> p -> p -> p -> p -> ()
d_IsStrictTotalOrder'7580'_604 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_IsStrictTotalOrder'7580'_604
  = C_constructor_638 MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                      (AgdaAny ->
                       AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158)
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ.isEquivalence
d_isEquivalence_614 ::
  T_IsStrictTotalOrder'7580'_604 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28
d_isEquivalence_614 :: T_IsStrictTotalOrder'7580'_604 -> T_IsEquivalence_28
d_isEquivalence_614 T_IsStrictTotalOrder'7580'_604
v0
  = case T_IsStrictTotalOrder'7580'_604 -> T_IsStrictTotalOrder'7580'_604
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_604
v0 of
      C_constructor_638 T_IsEquivalence_28
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> T_Tri_158
v3 -> T_IsEquivalence_28 -> T_IsEquivalence_28
forall a b. a -> b
coe T_IsEquivalence_28
v1
      T_IsStrictTotalOrder'7580'_604
_ -> T_IsEquivalence_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ.trans
d_trans_616 ::
  T_IsStrictTotalOrder'7580'_604 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_616 :: T_IsStrictTotalOrder'7580'_604
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_616 T_IsStrictTotalOrder'7580'_604
v0
  = case T_IsStrictTotalOrder'7580'_604 -> T_IsStrictTotalOrder'7580'_604
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_604
v0 of
      C_constructor_638 T_IsEquivalence_28
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'_604
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ.compare
d_compare_618 ::
  T_IsStrictTotalOrder'7580'_604 ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
d_compare_618 :: T_IsStrictTotalOrder'7580'_604 -> AgdaAny -> AgdaAny -> T_Tri_158
d_compare_618 T_IsStrictTotalOrder'7580'_604
v0
  = case T_IsStrictTotalOrder'7580'_604 -> T_IsStrictTotalOrder'7580'_604
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_604
v0 of
      C_constructor_638 T_IsEquivalence_28
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'_604
_ -> AgdaAny -> AgdaAny -> T_Tri_158
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Structures.Biased.IsStrictTotalOrderᶜ.isStrictTotalOrderᶜ
d_isStrictTotalOrder'7580'_620 ::
  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'_604 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624
d_isStrictTotalOrder'7580'_620 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_IsStrictTotalOrder'7580'_604
-> T_IsStrictTotalOrder_624
d_isStrictTotalOrder'7580'_620 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsStrictTotalOrder'7580'_604
v6
  = T_IsStrictTotalOrder'7580'_604 -> T_IsStrictTotalOrder_624
du_isStrictTotalOrder'7580'_620 T_IsStrictTotalOrder'7580'_604
v6
du_isStrictTotalOrder'7580'_620 ::
  T_IsStrictTotalOrder'7580'_604 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624
du_isStrictTotalOrder'7580'_620 :: T_IsStrictTotalOrder'7580'_604 -> T_IsStrictTotalOrder_624
du_isStrictTotalOrder'7580'_620 T_IsStrictTotalOrder'7580'_604
v0
  = (T_IsStrictPartialOrder_370
 -> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_624
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370
-> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Structures.C_constructor_680
      ((T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_370)
-> T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.C_constructor_412
         (T_IsStrictTotalOrder'7580'_604 -> T_IsEquivalence_28
d_isEquivalence_614 (T_IsStrictTotalOrder'7580'_604 -> T_IsStrictTotalOrder'7580'_604
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_604
v0)) (T_IsStrictTotalOrder'7580'_604
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans_616 (T_IsStrictTotalOrder'7580'_604 -> T_IsStrictTotalOrder'7580'_604
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_604
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_772
            ((T_IsStrictTotalOrder'7580'_604 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_604 -> AgdaAny -> AgdaAny -> T_Tri_158
d_compare_618 (T_IsStrictTotalOrder'7580'_604 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_604
v0))))
      ((T_IsStrictTotalOrder'7580'_604 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_604 -> AgdaAny -> AgdaAny -> T_Tri_158
d_compare_618 (T_IsStrictTotalOrder'7580'_604 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder'7580'_604
v0))