{-# 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'__96 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  AgdaAny -> AgdaAny -> ()
d__'8805'__96 :: T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
d__'8805'__96 = T_TotalPreorder_222 -> AgdaAny -> AgdaAny -> ()
forall a. a
erased
-- Algebra.Construct.NaturalChoice.Base._.MinOperator
d_MinOperator_98 :: p -> p -> p -> p -> ()
d_MinOperator_98 p
a0 p
a1 p
a2 p
a3 = ()
data T_MinOperator_98
  = C_MinOperator'46'constructor_1121 (AgdaAny -> AgdaAny -> AgdaAny)
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Algebra.Construct.NaturalChoice.Base._.MinOperator._⊓_
d__'8851'__114 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__114 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__114 T_MinOperator_98
v0
  = case T_MinOperator_98 -> T_MinOperator_98
forall a b. a -> b
coe T_MinOperator_98
v0 of
      C_MinOperator'46'constructor_1121 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_98
_ -> 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_120 ::
  T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_120 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_120 T_MinOperator_98
v0
  = case T_MinOperator_98 -> T_MinOperator_98
forall a b. a -> b
coe T_MinOperator_98
v0 of
      C_MinOperator'46'constructor_1121 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_98
_ -> 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_126 ::
  T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_126 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_126 T_MinOperator_98
v0
  = case T_MinOperator_98 -> T_MinOperator_98
forall a b. a -> b
coe T_MinOperator_98
v0 of
      C_MinOperator'46'constructor_1121 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_98
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Construct.NaturalChoice.Base._.MaxOperator
d_MaxOperator_128 :: p -> p -> p -> p -> ()
d_MaxOperator_128 p
a0 p
a1 p
a2 p
a3 = ()
data T_MaxOperator_128
  = C_MaxOperator'46'constructor_1665 (AgdaAny -> AgdaAny -> AgdaAny)
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-- Algebra.Construct.NaturalChoice.Base._.MaxOperator._⊔_
d__'8852'__144 ::
  T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__144 :: T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__144 T_MaxOperator_128
v0
  = case T_MaxOperator_128 -> T_MaxOperator_128
forall a b. a -> b
coe T_MaxOperator_128
v0 of
      C_MaxOperator'46'constructor_1665 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_128
_ -> 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_150 ::
  T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_150 :: T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_150 T_MaxOperator_128
v0
  = case T_MaxOperator_128 -> T_MaxOperator_128
forall a b. a -> b
coe T_MaxOperator_128
v0 of
      C_MaxOperator'46'constructor_1665 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_128
_ -> 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_156 ::
  T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_156 :: T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_156 T_MaxOperator_128
v0
  = case T_MaxOperator_128 -> T_MaxOperator_128
forall a b. a -> b
coe T_MaxOperator_128
v0 of
      C_MaxOperator'46'constructor_1665 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_128
_ -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algebra.Construct.NaturalChoice.Base.MinOp⇒MaxOp
d_MinOp'8658'MaxOp_158 ::
  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_222 ->
  T_MinOperator_98 -> T_MaxOperator_128
d_MinOp'8658'MaxOp_158 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_MaxOperator_128
d_MinOp'8658'MaxOp_158 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_222
v3 T_MinOperator_98
v4
  = T_MinOperator_98 -> T_MaxOperator_128
du_MinOp'8658'MaxOp_158 T_MinOperator_98
v4
du_MinOp'8658'MaxOp_158 :: T_MinOperator_98 -> T_MaxOperator_128
du_MinOp'8658'MaxOp_158 :: T_MinOperator_98 -> T_MaxOperator_128
du_MinOp'8658'MaxOp_158 T_MinOperator_98
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_MaxOperator_128)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_MaxOperator_128
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MaxOperator_128
C_MaxOperator'46'constructor_1665 ((T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__114 (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v0))
      ((T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_126 (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v0))
      ((T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_120 (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v0))
-- Algebra.Construct.NaturalChoice.Base._._._⊓_
d__'8851'__168 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__168 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__168 T_MinOperator_98
v0 = (T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8851'__114 (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v0)
-- Algebra.Construct.NaturalChoice.Base._._.x≤y⇒x⊓y≈x
d_x'8804'y'8658'x'8851'y'8776'x_170 ::
  T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_170 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_170 T_MinOperator_98
v0
  = (T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8851'y'8776'x_120 (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v0)
-- Algebra.Construct.NaturalChoice.Base._._.x≥y⇒x⊓y≈y
d_x'8805'y'8658'x'8851'y'8776'y_172 ::
  T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_172 :: T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_172 T_MinOperator_98
v0
  = (T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8851'y'8776'y_126 (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v0)
-- Algebra.Construct.NaturalChoice.Base.MaxOp⇒MinOp
d_MaxOp'8658'MinOp_174 ::
  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_222 ->
  T_MaxOperator_128 -> T_MinOperator_98
d_MaxOp'8658'MinOp_174 :: ()
-> ()
-> ()
-> T_TotalPreorder_222
-> T_MaxOperator_128
-> T_MinOperator_98
d_MaxOp'8658'MinOp_174 ~()
v0 ~()
v1 ~()
v2 ~T_TotalPreorder_222
v3 T_MaxOperator_128
v4
  = T_MaxOperator_128 -> T_MinOperator_98
du_MaxOp'8658'MinOp_174 T_MaxOperator_128
v4
du_MaxOp'8658'MinOp_174 :: T_MaxOperator_128 -> T_MinOperator_98
du_MaxOp'8658'MinOp_174 :: T_MaxOperator_128 -> T_MinOperator_98
du_MaxOp'8658'MinOp_174 T_MaxOperator_128
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_MinOperator_98)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_MinOperator_98
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_MinOperator_98
C_MinOperator'46'constructor_1121 ((T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__144 (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v0))
      ((T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_156 (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v0))
      ((T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_150 (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v0))
-- Algebra.Construct.NaturalChoice.Base._._._⊔_
d__'8852'__184 ::
  T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__184 :: T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__184 T_MaxOperator_128
v0 = (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8852'__144 (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v0)
-- Algebra.Construct.NaturalChoice.Base._._.x≤y⇒x⊔y≈y
d_x'8804'y'8658'x'8852'y'8776'y_186 ::
  T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_186 :: T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_186 T_MaxOperator_128
v0
  = (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8804'y'8658'x'8852'y'8776'y_150 (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v0)
-- Algebra.Construct.NaturalChoice.Base._._.x≥y⇒x⊔y≈x
d_x'8805'y'8658'x'8852'y'8776'x_188 ::
  T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_188 :: T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_188 T_MaxOperator_128
v0
  = (T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_x'8805'y'8658'x'8852'y'8776'x_156 (T_MaxOperator_128 -> AgdaAny
forall a b. a -> b
coe T_MaxOperator_128
v0)