content: {-# 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.MaxOp where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Algebra.Construct.NaturalChoice.Base qualified
  import MAlonzo.Code.Algebra.Lattice.Bundles qualified
  import MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp qualified
  import MAlonzo.Code.Algebra.Structures qualified
  import MAlonzo.Code.Relation.Binary.Bundles qualified
  import MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd 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.MaxOp.Min.⊓-isSemilattice
  d_'8851''45'isSemilattice_22 ::
    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_MaxOperator_128 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  d_'8851''45'isSemilattice_22 ~v0 ~v1 ~v2 v3 v4
    = du_'8851''45'isSemilattice_22 v3 v4
  du_'8851''45'isSemilattice_22 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
    MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
    MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
  du_'8851''45'isSemilattice_22 v0 v1
    = coe
        MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'isSemilattice_602
        (coe
           MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
           (coe v0))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
           (coe v1))
  -- Algebra.Lattice.Construct.NaturalChoice.MaxOp.Min.⊓-semilattice
  d_'8851''45'semilattice_24 ::
    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_MaxOperator_128 ->
    MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
  d_'8851''45'semilattice_24 ~v0 ~v1 ~v2 v3 v4
    = du_'8851''45'semilattice_24 v3 v4
  du_'8851''45'semilattice_24 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_TotalPreorder_222 ->
    MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.T_MaxOperator_128 ->
    MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
  du_'8851''45'semilattice_24 v0 v1
    = coe
        MAlonzo.Code.Algebra.Lattice.Construct.NaturalChoice.MinOp.du_'8851''45'semilattice_604
        (coe
           MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd.du_totalPreorder_746
           (coe v0))
        (coe
           MAlonzo.Code.Algebra.Construct.NaturalChoice.Base.du_MaxOp'8658'MinOp_174
           (coe v1))
  