{-# 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.Algebra.Construct.NaturalChoice.Base 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.Bundles

-- Algebra.Construct.NaturalChoice.Base._._≥_
d__'8805'__82 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  AgdaAny -> AgdaAny -> ()
d__'8805'__82 :: T_TotalPreorder_204 -> AgdaAny -> AgdaAny -> ()
d__'8805'__82 = T_TotalPreorder_204 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Construct.NaturalChoice.Base._.MinOperator
d_MinOperator_84 :: p -> p -> p -> p -> ()
d_MinOperator_84 p
a0 p
a1 p
a2 p
a3 = ()
data T_MinOperator_84
  = C_MinOperator'46'constructor_983 (AgdaAny -> AgdaAny -> AgdaAny)
                                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                     (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Algebra.Construct.NaturalChoice.Base._.MinOperator._⊓_
d__'8851'__100 :: T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__100 :: T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__100 T_MinOperator_84
v0
  = case T_MinOperator_84 -> T_MinOperator_84
forall a b. a -> b
coe T_MinOperator_84
v0 of
      C_MinOperator'46'constructor_983 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1
      T_MinOperator_84
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Construct.NaturalChoice.Base._.MinOperator.x≤y⇒x⊓y≈x
d_x'8804'y'8658'x'8851'y'8776'x_106 ::
  T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_106 :: T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_106 T_MinOperator_84
v0
  = case T_MinOperator_84 -> T_MinOperator_84
forall a b. a -> b
coe T_MinOperator_84
v0 of
      C_MinOperator'46'constructor_983 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_MinOperator_84
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Construct.NaturalChoice.Base._.MinOperator.x≥y⇒x⊓y≈y
d_x'8805'y'8658'x'8851'y'8776'y_112 ::
  T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_112 :: T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_112 T_MinOperator_84
v0
  = case T_MinOperator_84 -> T_MinOperator_84
forall a b. a -> b
coe T_MinOperator_84
v0 of
      C_MinOperator'46'constructor_983 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
      T_MinOperator_84
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Construct.NaturalChoice.Base._.MaxOperator
d_MaxOperator_114 :: p -> p -> p -> p -> ()
d_MaxOperator_114 p
a0 p
a1 p
a2 p
a3 = ()
data T_MaxOperator_114
  = C_MaxOperator'46'constructor_1521 (AgdaAny -> AgdaAny -> AgdaAny)
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Algebra.Construct.NaturalChoice.Base._.MaxOperator._⊔_
d__'8852'__130 ::
  T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__130 :: T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__130 T_MaxOperator_114
v0
  = case T_MaxOperator_114 -> T_MaxOperator_114
forall a b. a -> b
coe T_MaxOperator_114
v0 of
      C_MaxOperator'46'constructor_1521 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1
      T_MaxOperator_114
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Construct.NaturalChoice.Base._.MaxOperator.x≤y⇒x⊔y≈y
d_x'8804'y'8658'x'8852'y'8776'y_136 ::
  T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_136 :: T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_136 T_MaxOperator_114
v0
  = case T_MaxOperator_114 -> T_MaxOperator_114
forall a b. a -> b
coe T_MaxOperator_114
v0 of
      C_MaxOperator'46'constructor_1521 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      T_MaxOperator_114
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Construct.NaturalChoice.Base._.MaxOperator.x≥y⇒x⊔y≈x
d_x'8805'y'8658'x'8852'y'8776'x_142 ::
  T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_142 :: T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_142 T_MaxOperator_114
v0
  = case T_MaxOperator_114 -> T_MaxOperator_114
forall a b. a -> b
coe T_MaxOperator_114
v0 of
      C_MaxOperator'46'constructor_1521 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3
      T_MaxOperator_114
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Construct.NaturalChoice.Base.MinOp⇒MaxOp
d_MinOp'8658'MaxOp_144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  T_MinOperator_84 -> T_MaxOperator_114
d_MinOp'8658'MaxOp_144 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MinOperator_84
-> T_MaxOperator_114
d_MinOp'8658'MaxOp_144 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_204
v3 T_MinOperator_84
v4
  = T_MinOperator_84 -> T_MaxOperator_114
du_MinOp'8658'MaxOp_144 T_MinOperator_84
v4
du_MinOp'8658'MaxOp_144 :: T_MinOperator_84 -> T_MaxOperator_114
du_MinOp'8658'MaxOp_144 :: T_MinOperator_84 -> T_MaxOperator_114
du_MinOp'8658'MaxOp_144 T_MinOperator_84
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_MaxOperator_114)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_MaxOperator_114
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_114
C_MaxOperator'46'constructor_1521 ((T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__100 (T_MinOperator_84 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84
v0))
      ((T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_112 (T_MinOperator_84 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84
v0))
      ((T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_106 (T_MinOperator_84 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84
v0))
-- Algebra.Construct.NaturalChoice.Base._._._⊓_
d__'8851'__154 :: T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__154 :: T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__154 T_MinOperator_84
v0 = (T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__100 (T_MinOperator_84 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84
v0)
-- Algebra.Construct.NaturalChoice.Base._._.x≤y⇒x⊓y≈x
d_x'8804'y'8658'x'8851'y'8776'x_156 ::
  T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_156 :: T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_156 T_MinOperator_84
v0
  = (T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_106 (T_MinOperator_84 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84
v0)
-- Algebra.Construct.NaturalChoice.Base._._.x≥y⇒x⊓y≈y
d_x'8805'y'8658'x'8851'y'8776'y_158 ::
  T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_158 :: T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_158 T_MinOperator_84
v0
  = (T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_112 (T_MinOperator_84 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_84
v0)
-- Algebra.Construct.NaturalChoice.Base.MaxOp⇒MinOp
d_MaxOp'8658'MinOp_160 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_204 ->
  T_MaxOperator_114 -> T_MinOperator_84
d_MaxOp'8658'MinOp_160 :: ()
-> ()
-> ()
-> T_TotalPreorder_204
-> T_MaxOperator_114
-> T_MinOperator_84
d_MaxOp'8658'MinOp_160 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_204
v3 T_MaxOperator_114
v4
  = T_MaxOperator_114 -> T_MinOperator_84
du_MaxOp'8658'MinOp_160 T_MaxOperator_114
v4
du_MaxOp'8658'MinOp_160 :: T_MaxOperator_114 -> T_MinOperator_84
du_MaxOp'8658'MinOp_160 :: T_MaxOperator_114 -> T_MinOperator_84
du_MaxOp'8658'MinOp_160 T_MaxOperator_114
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_MinOperator_84)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_MinOperator_84
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MinOperator_84
C_MinOperator'46'constructor_983 ((T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__130 (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v0))
      ((T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_142 (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v0))
      ((T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_136 (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v0))
-- Algebra.Construct.NaturalChoice.Base._._._⊔_
d__'8852'__170 ::
  T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__170 :: T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__170 T_MaxOperator_114
v0 = (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__130 (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v0)
-- Algebra.Construct.NaturalChoice.Base._._.x≤y⇒x⊔y≈y
d_x'8804'y'8658'x'8852'y'8776'y_172 ::
  T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_172 :: T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_172 T_MaxOperator_114
v0
  = (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_136 (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v0)
-- Algebra.Construct.NaturalChoice.Base._._.x≥y⇒x⊔y≈x
d_x'8805'y'8658'x'8852'y'8776'x_174 ::
  T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_174 :: T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_174 T_MaxOperator_114
v0
  = (T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_142 (T_MaxOperator_114 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_114
v0)