{-# 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.Lattice.Construct.NaturalChoice.MinOp where

import Data.Text qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Algebra.Construct.NaturalChoice.Base qualified
import MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp qualified
import MAlonzo.Code.Algebra.Lattice.Bundles qualified
import MAlonzo.Code.Algebra.Structures qualified
import MAlonzo.Code.Relation.Binary.Bundles 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

-- Algebra.Lattice.Construct.NaturalChoice.MinOp._.IsSemilattice
d_IsSemilattice_114 ::
  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 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_IsSemilattice_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalPreorder_222
-> T_MinOperator_98
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_IsSemilattice_114 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalPreorder_222
-> T_MinOperator_98
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Construct.NaturalChoice.MinOp.⊓-isSemilattice
d_'8851''45'isSemilattice_602 ::
  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 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
d_'8851''45'isSemilattice_602 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_IsCommutativeBand_590
d_'8851''45'isSemilattice_602 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4
  = T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsCommutativeBand_590
du_'8851''45'isSemilattice_602 T_TotalPreorder_222
v3 T_MinOperator_98
v4
du_'8851''45'isSemilattice_602 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
du_'8851''45'isSemilattice_602 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsCommutativeBand_590
du_'8851''45'isSemilattice_602 T_TotalPreorder_222
v0 T_MinOperator_98
v1
  = (T_IsBand_508
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_590
forall a b. a -> b
coe
      T_IsBand_508
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_590
MAlonzo.Code.Algebra.Structures.C_IsCommutativeBand'46'constructor_13109
      ((T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsBand_508)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsBand_508
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isBand_3034
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_222
-> T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2856
         (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1))
-- Algebra.Lattice.Construct.NaturalChoice.MinOp.⊓-semilattice
d_'8851''45'semilattice_604 ::
  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 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8851''45'semilattice_604 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalPreorder_222
-> T_MinOperator_98
-> T_Semilattice_10
d_'8851''45'semilattice_604 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalPreorder_222
v3 T_MinOperator_98
v4
  = T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semilattice_10
du_'8851''45'semilattice_604 T_TotalPreorder_222
v3 T_MinOperator_98
v4
du_'8851''45'semilattice_604 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_98 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8851''45'semilattice_604 :: T_TotalPreorder_222 -> T_MinOperator_98 -> T_Semilattice_10
du_'8851''45'semilattice_604 T_TotalPreorder_222
v0 T_MinOperator_98
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_590 -> T_Semilattice_10)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_590 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Bundles.C_Semilattice'46'constructor_193
      (T_MinOperator_98 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__114
         (T_MinOperator_98 -> T_MinOperator_98
forall a b. a -> b
coe T_MinOperator_98
v1))
      ((T_TotalPreorder_222
 -> T_MinOperator_98 -> T_IsCommutativeBand_590)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222 -> T_MinOperator_98 -> T_IsCommutativeBand_590
du_'8851''45'isSemilattice_602 (T_TotalPreorder_222 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_222
v0) (T_MinOperator_98 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_98
v1))