{-# 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_210 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> ()
d_IsSemilattice_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalPreorder_240
-> T_MinOperator_106
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
d_IsSemilattice_210 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalPreorder_240
-> T_MinOperator_106
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Level_18
forall a. a
erased
-- Algebra.Lattice.Construct.NaturalChoice.MinOp.⊓-isSemilattice
d_'8851''45'isSemilattice_616 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
d_'8851''45'isSemilattice_616 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_IsCommutativeBand_612
d_'8851''45'isSemilattice_616 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4
  = T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsCommutativeBand_612
du_'8851''45'isSemilattice_616 T_TotalPreorder_240
v3 T_MinOperator_106
v4
du_'8851''45'isSemilattice_616 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_612
du_'8851''45'isSemilattice_616 :: T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsCommutativeBand_612
du_'8851''45'isSemilattice_616 T_TotalPreorder_240
v0 T_MinOperator_106
v1
  = (T_IsBand_526
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_612)
-> AgdaAny -> AgdaAny -> T_IsCommutativeBand_612
forall a b. a -> b
coe
      T_IsBand_526
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsCommutativeBand_612
MAlonzo.Code.Algebra.Structures.C_constructor_660
      ((T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsBand_526)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsBand_526
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'isBand_3150
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalPreorder_240
-> T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp.du_'8851''45'comm_2972
         (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1))
-- Algebra.Lattice.Construct.NaturalChoice.MinOp.⊓-semilattice
d_'8851''45'semilattice_618 ::
  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_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8851''45'semilattice_618 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalPreorder_240
-> T_MinOperator_106
-> T_Semilattice_10
d_'8851''45'semilattice_618 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalPreorder_240
v3 T_MinOperator_106
v4
  = T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semilattice_10
du_'8851''45'semilattice_618 T_TotalPreorder_240
v3 T_MinOperator_106
v4
du_'8851''45'semilattice_618 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_240 ->
  MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MinOperator_106 ->
  MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
du_'8851''45'semilattice_618 :: T_TotalPreorder_240 -> T_MinOperator_106 -> T_Semilattice_10
du_'8851''45'semilattice_618 T_TotalPreorder_240
v0 T_MinOperator_106
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsCommutativeBand_612 -> T_Semilattice_10)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Semilattice_10
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsCommutativeBand_612 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Bundles.C_constructor_84
      (T_MinOperator_106 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.d__'8851'__122
         (T_MinOperator_106 -> T_MinOperator_106
forall a b. a -> b
coe T_MinOperator_106
v1))
      ((T_TotalPreorder_240
 -> T_MinOperator_106 -> T_IsCommutativeBand_612)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240 -> T_MinOperator_106 -> T_IsCommutativeBand_612
du_'8851''45'isSemilattice_616 (T_TotalPreorder_240 -> AgdaAny
forall a b. a -> b
coe T_TotalPreorder_240
v0) (T_MinOperator_106 -> AgdaAny
forall a b. a -> b
coe T_MinOperator_106
v1))