{-# 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 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.Algebra.Construct.NaturalChoice.Base
import qualified MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp
import qualified MAlonzo.Code.Algebra.Lattice.Bundles
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Relation.Binary.Bundles

-- 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))