{-# 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.Data.List.Extrema 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.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.Extrema.Core
import qualified MAlonzo.Code.Data.List.Membership.Propositional
import qualified MAlonzo.Code.Data.List.Membership.Propositional.Properties
import qualified MAlonzo.Code.Data.List.Membership.Setoid.Properties
import qualified MAlonzo.Code.Data.List.Properties
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.Data.List.Relation.Unary.Any
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Data.List.Extrema._._<_
d__'60'__80 ::
  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_TotalOrder_652 ->
  AgdaAny -> AgdaAny -> ()
d__'60'__80 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__80 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.List.Extrema.argmin
d_argmin_118 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmin_118 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmin_118 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_118 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6
du_argmin_118 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_118 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_118 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_338 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
-- Data.List.Extrema.argmax
d_argmax_122 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmax_122 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmax_122 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_122 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6
du_argmax_122 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_122 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_122 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_340 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
-- Data.List.Extrema.min
d_min_126 ::
  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_TotalOrder_652 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_min_126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_min_126 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min_126 T_TotalOrder_652
v3
du_min_126 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_min_126 :: T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min_126 T_TotalOrder_652
v0 = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_118 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.max
d_max_128 ::
  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_TotalOrder_652 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_max_128 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_max_128 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_max_128 T_TotalOrder_652
v3
du_max_128 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_max_128 :: T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_max_128 T_TotalOrder_652
v0 = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_122 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema._.f[argmin]≤v⁺
d_f'91'argmin'93''8804'v'8314'_146 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_f'91'argmin'93''8804'v'8314'_146 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_f'91'argmin'93''8804'v'8314'_146 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_146 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_f'91'argmin'93''8804'v'8314'_146 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_f'91'argmin'93''8804'v'8314'_146 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_146 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_2826
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_338 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7506''45''8804'v_356
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.f[argmin]<v⁺
d_f'91'argmin'93''60'v'8314'_156 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_f'91'argmin'93''60'v'8314'_156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_f'91'argmin'93''60'v'8314'_156 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_156 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_f'91'argmin'93''60'v'8314'_156 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_f'91'argmin'93''60'v'8314'_156 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_156 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_2826
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_338 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7506''45''60'v_368
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.v≤f[argmin]⁺
d_v'8804'f'91'argmin'93''8314'_166 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_v'8804'f'91'argmin'93''8314'_166 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_v'8804'f'91'argmin'93''8314'_166 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                   [AgdaAny]
v9
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_166 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_v'8804'f'91'argmin'93''8314'_166 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_v'8804'f'91'argmin'93''8314'_166 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_166 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_2786
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_338 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7495''45'v'8804'_380
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.v<f[argmin]⁺
d_v'60'f'91'argmin'93''8314'_176 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'f'91'argmin'93''8314'_176 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_v'60'f'91'argmin'93''8314'_176 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                 [AgdaAny]
v9
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_176 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_v'60'f'91'argmin'93''8314'_176 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'f'91'argmin'93''8314'_176 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_176 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_2786
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_338 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7495''45'v'60'_396
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.f[argmin]≤f[⊤]
d_f'91'argmin'93''8804'f'91''8868''93'_182 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_f'91'argmin'93''8804'f'91''8868''93'_182 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_f'91'argmin'93''8804'f'91''8868''93'_182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                           AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_182 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91'argmin'93''8804'f'91''8868''93'_182 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_182 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_182 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_146 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v2 [AgdaAny]
v3
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
         (let v4 :: T_IsTotalOrder_384
v4
                = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                    (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsPartialOrder_162
v5
                   = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                       (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                  ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v5))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))
-- Data.List.Extrema._.f[argmin]≤f[xs]
d_f'91'argmin'93''8804'f'91'xs'93'_194 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_f'91'argmin'93''8804'f'91'xs'93'_194 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'argmin'93''8804'f'91'xs'93'_194 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
                                       [AgdaAny]
v8
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_194 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91'argmin'93''8804'f'91'xs'93'_194 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_194 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_194 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
MAlonzo.Code.Data.List.Properties.du_foldr'45'forces'7495'_2752
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_338 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'forces'7495''45'v'8804'_412
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_118 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
      (let v4 :: T_IsTotalOrder_384
v4
             = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                 (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: T_IsPartialOrder_162
v5
                = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v4) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
               ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v5))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_118 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3)))))
-- Data.List.Extrema._.f[argmin]≈f[v]⁺
d_f'91'argmin'93''8776'f'91'v'93''8314'_208 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_f'91'argmin'93''8776'f'91'v'93''8314'_208 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_f'91'argmin'93''8776'f'91'v'93''8314'_208 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_208
      T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
du_f'91'argmin'93''8776'f'91'v'93''8314'_208 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_208 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_208 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 [AgdaAny]
v4 T_Any_34
v5 T_All_44
v6
                                             AgdaAny
v7
  = (T_IsPartialOrder_162
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
      (T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
         ((T_TotalOrder_652 -> T_IsTotalOrder_384)
-> AgdaAny -> T_IsTotalOrder_384
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_118 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_146 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v3 [AgdaAny]
v4
         ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
            ((AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Membership.Propositional.du_lose_54 AgdaAny
v2 [AgdaAny]
v4 T_Any_34
v5
               (let v8 :: T_IsTotalOrder_384
v8
                      = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                          (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v9 :: T_IsPartialOrder_162
v9
                         = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                             (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v8) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                        ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v9))
                        ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))))
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_166 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4 AgdaAny
v7 T_All_44
v6)
-- Data.List.Extrema.argmin[xs]≤argmin[ys]⁺
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
                                                   ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234
      T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
                                                    [AgdaAny]
v5 [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_166 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v2 AgdaAny
v4 [AgdaAny]
v6
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_146 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4) AgdaAny
v3 [AgdaAny]
v5 T__'8846'__30
v7)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_166
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v9 ->
               (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_146 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v9) AgdaAny
v3 [AgdaAny]
v5))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmin[xs]<argmin[ys]⁺
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4
                                                 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262
      T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 [AgdaAny]
v5
                                                  [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_176 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v2 AgdaAny
v4 [AgdaAny]
v6
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_156 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4) AgdaAny
v3 [AgdaAny]
v5 T__'8846'__30
v7)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_166
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v9 ->
               (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_156 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v9) AgdaAny
v3 [AgdaAny]
v5))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmin-sel
d_argmin'45'sel_278 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmin'45'sel_278 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmin'45'sel_278 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmin'45'sel_278 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6
du_argmin'45'sel_278 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_argmin'45'sel_278 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmin'45'sel_278 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Propositional.Properties.du_foldr'45'selective_674
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_338 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'sel_344
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
-- Data.List.Extrema.argmin-all
d_argmin'45'all_290 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmin'45'all_290 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_All_44
-> AgdaAny
d_argmin'45'all_290 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 ~AgdaAny -> T_Level_18
v10 AgdaAny
v11
                    T_All_44
v12
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmin'45'all_290 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 AgdaAny
v11 T_All_44
v12
du_argmin'45'all_290 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmin'45'all_290 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmin'45'all_290 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 AgdaAny
v4 T_All_44
v5
  = let v6 :: t
v6
          = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
              T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Setoid.Properties.du_foldr'45'selective_1660
              (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                 T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
              ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_338 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
              ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'sel_344
                 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v6 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
           -> ([AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                [AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny
MAlonzo.Code.Data.List.Relation.Unary.All.du_lookup_434 [AgdaAny]
v3 T_All_44
v5 AgdaAny
v7
         T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.List.Extrema._.v≤f[argmax]⁺
d_v'8804'f'91'argmax'93''8314'_352 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_v'8804'f'91'argmax'93''8314'_352 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_v'8804'f'91'argmax'93''8314'_352 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_352 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_v'8804'f'91'argmax'93''8314'_352 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_v'8804'f'91'argmax'93''8314'_352 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_352 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_2826
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_340 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7506''45'v'8804'_440
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.v<f[argmax]⁺
d_v'60'f'91'argmax'93''8314'_362 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'f'91'argmax'93''8314'_362 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_v'60'f'91'argmax'93''8314'_362 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_362 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_v'60'f'91'argmax'93''8314'_362 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'f'91'argmax'93''8314'_362 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_362 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_2826
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_340 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7506''45'v'60'_462
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.f[argmax]≤v⁺
d_f'91'argmax'93''8804'v'8314'_372 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_f'91'argmax'93''8804'v'8314'_372 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_f'91'argmax'93''8804'v'8314'_372 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                   [AgdaAny]
v9
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_372 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_f'91'argmax'93''8804'v'8314'_372 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_f'91'argmax'93''8804'v'8314'_372 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_372 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_2786
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_340 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7495''45''8804'v_484
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.f[argmax]<v⁺
d_f'91'argmax'93''60'v'8314'_382 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_f'91'argmax'93''60'v'8314'_382 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_f'91'argmax'93''60'v'8314'_382 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                 [AgdaAny]
v9
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_382 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_f'91'argmax'93''60'v'8314'_382 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_f'91'argmax'93''60'v'8314'_382 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_382 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_2786
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_340 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7495''45''60'v_500
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.f[⊥]≤f[argmax]
d_f'91''8869''93''8804'f'91'argmax'93'_388 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_f'91''8869''93''8804'f'91'argmax'93'_388 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_f'91''8869''93''8804'f'91'argmax'93'_388 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                           AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_388 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91''8869''93''8804'f'91'argmax'93'_388 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_388 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_388 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_352 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v2 [AgdaAny]
v3
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
         (let v4 :: T_IsTotalOrder_384
v4
                = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                    (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: T_IsPartialOrder_162
v5
                   = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                       (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v4) in
             AgdaAny -> AgdaAny
forall a b. a -> b
coe
               ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                  ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v5))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))
-- Data.List.Extrema._.f[xs]≤f[argmax]
d_f'91'xs'93''8804'f'91'argmax'93'_400 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_f'91'xs'93''8804'f'91'argmax'93'_400 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'xs'93''8804'f'91'argmax'93'_400 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
                                       [AgdaAny]
v8
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_400 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91'xs'93''8804'f'91'argmax'93'_400 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_400 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_400 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
MAlonzo.Code.Data.List.Properties.du_foldr'45'forces'7495'_2752
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_340 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'forces'7495''45''8804'v_516
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_122 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
      (let v4 :: T_IsTotalOrder_384
v4
             = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                 (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v5 :: T_IsPartialOrder_162
v5
                = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                    (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v4) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
               ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v5))
               ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  AgdaAny -> AgdaAny
v1
                  (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
                     ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_340 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))))))
-- Data.List.Extrema._.f[argmax]≈f[v]⁺
d_f'91'argmax'93''8776'f'91'v'93''8314'_414 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_f'91'argmax'93''8776'f'91'v'93''8314'_414 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_f'91'argmax'93''8776'f'91'v'93''8314'_414 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_414
      T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
du_f'91'argmax'93''8776'f'91'v'93''8314'_414 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_414 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_414 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 [AgdaAny]
v4 T_Any_34
v5 T_All_44
v6
                                             AgdaAny
v7
  = (T_IsPartialOrder_162
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_172
      (T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
         ((T_TotalOrder_652 -> T_IsTotalOrder_384)
-> AgdaAny -> T_IsTotalOrder_384
forall a b. a -> b
coe
            T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_122 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_372 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4 AgdaAny
v7 T_All_44
v6)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_352 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v3 [AgdaAny]
v4
         ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
            ((AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Membership.Propositional.du_lose_54 AgdaAny
v2 [AgdaAny]
v4 T_Any_34
v5
               (let v8 :: T_IsTotalOrder_384
v8
                      = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
                          (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  (let v9 :: T_IsPartialOrder_162
v9
                         = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                             (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v8) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
                        ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v9))
                        ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))))
-- Data.List.Extrema.argmax[xs]≤argmax[ys]⁺
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
                                                   ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440
      T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
                                                    [AgdaAny]
v5 [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_372 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v5
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_352 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4 [AgdaAny]
v6 T__'8846'__30
v7)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_166
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v9 ->
               (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_352 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v9) AgdaAny
v4 [AgdaAny]
v6))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmax[xs]<argmax[ys]⁺
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4
                                                 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468
      T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 [AgdaAny]
v5
                                                  [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_382 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v5
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_362 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4 [AgdaAny]
v6 T__'8846'__30
v7)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_166
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v9 ->
               (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_362 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v9) AgdaAny
v4 [AgdaAny]
v6))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmax-sel
d_argmax'45'sel_484 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmax'45'sel_484 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmax'45'sel_484 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmax'45'sel_484 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v6
du_argmax'45'sel_484 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_argmax'45'sel_484 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmax'45'sel_484 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Propositional.Properties.du_foldr'45'selective_674
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_340 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'sel_428
         (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
-- Data.List.Extrema.argmax-all
d_argmax'45'all_496 ::
  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_TotalOrder_652 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmax'45'all_496 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_argmax'45'all_496 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 AgdaAny -> AgdaAny
v7 ~AgdaAny -> T_Level_18
v8 AgdaAny
v9 [AgdaAny]
v10 AgdaAny
v11
                    T_All_44
v12
  = T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmax'45'all_496 T_TotalOrder_652
v3 AgdaAny -> AgdaAny
v7 AgdaAny
v9 [AgdaAny]
v10 AgdaAny
v11 T_All_44
v12
du_argmax'45'all_496 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmax'45'all_496 :: T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmax'45'all_496 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 AgdaAny
v4 T_All_44
v5
  = let v6 :: t
v6
          = (T_Setoid_44
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
              T_Setoid_44
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Setoid.Properties.du_foldr'45'selective_1660
              (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
                 T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_250)
              ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_652 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_340 T_TotalOrder_652
v0 AgdaAny -> AgdaAny
v1)
              ((T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'sel_428
                 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v6 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
           -> ([AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                [AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny
MAlonzo.Code.Data.List.Relation.Unary.All.du_lookup_434 [AgdaAny]
v3 T_All_44
v5 AgdaAny
v7
         T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.List.Extrema.min≤v⁺
d_min'8804'v'8314'_550 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_min'8804'v'8314'_550 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_min'8804'v'8314'_550 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4
  = T_TotalOrder_652
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_min'8804'v'8314'_550 T_TotalOrder_652
v3 AgdaAny
v4
du_min'8804'v'8314'_550 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_min'8804'v'8314'_550 :: T_TotalOrder_652
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_min'8804'v'8314'_550 T_TotalOrder_652
v0 AgdaAny
v1
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_146 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.min<v⁺
d_min'60'v'8314'_560 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_min'60'v'8314'_560 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_min'60'v'8314'_560 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4
  = T_TotalOrder_652
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_min'60'v'8314'_560 T_TotalOrder_652
v3 AgdaAny
v4
du_min'60'v'8314'_560 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_min'60'v'8314'_560 :: T_TotalOrder_652
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_min'60'v'8314'_560 T_TotalOrder_652
v0 AgdaAny
v1
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_156 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.v≤min⁺
d_v'8804'min'8314'_570 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_v'8804'min'8314'_570 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_v'8804'min'8314'_570 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_652
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_v'8804'min'8314'_570 T_TotalOrder_652
v3 AgdaAny
v5 [AgdaAny]
v6
du_v'8804'min'8314'_570 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_v'8804'min'8314'_570 :: T_TotalOrder_652
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_v'8804'min'8314'_570 T_TotalOrder_652
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_166 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.v<min⁺
d_v'60'min'8314'_580 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'min'8314'_580 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_v'60'min'8314'_580 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_652
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_v'60'min'8314'_580 T_TotalOrder_652
v3 AgdaAny
v5 [AgdaAny]
v6
du_v'60'min'8314'_580 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'min'8314'_580 :: T_TotalOrder_652
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_v'60'min'8314'_580 T_TotalOrder_652
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_176 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.min≤⊤
d_min'8804''8868'_586 ::
  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_TotalOrder_652 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_min'8804''8868'_586 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_min'8804''8868'_586 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min'8804''8868'_586 T_TotalOrder_652
v3
du_min'8804''8868'_586 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_min'8804''8868'_586 :: T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min'8804''8868'_586 T_TotalOrder_652
v0
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_182 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min≤xs
d_min'8804'xs_594 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_min'8804'xs_594 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_min'8804'xs_594 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> T_All_44
du_min'8804'xs_594 T_TotalOrder_652
v3
du_min'8804'xs_594 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_min'8804'xs_594 :: T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> T_All_44
du_min'8804'xs_594 T_TotalOrder_652
v0
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_194 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min≈v⁺
d_min'8776'v'8314'_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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_min'8776'v'8314'_604 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_min'8776'v'8314'_604 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_min'8776'v'8314'_604 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
du_min'8776'v'8314'_604 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_min'8776'v'8314'_604 :: T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_min'8776'v'8314'_604 T_TotalOrder_652
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T_Any_34
 -> T_All_44
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_208 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
v4)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema.min[xs]≤min[ys]⁺
d_min'91'xs'93''8804'min'91'ys'93''8314'_620 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_min'91'xs'93''8804'min'91'ys'93''8314'_620 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_min'91'xs'93''8804'min'91'ys'93''8314'_620 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_620 T_TotalOrder_652
v3
du_min'91'xs'93''8804'min'91'ys'93''8314'_620 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_620 :: T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_620 T_TotalOrder_652
v0
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min[xs]<min[ys]⁺
d_min'91'xs'93''60'min'91'ys'93''8314'_636 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_min'91'xs'93''60'min'91'ys'93''8314'_636 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_min'91'xs'93''60'min'91'ys'93''8314'_636 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3
  = T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_min'91'xs'93''60'min'91'ys'93''8314'_636 T_TotalOrder_652
v3
du_min'91'xs'93''60'min'91'ys'93''8314'_636 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_min'91'xs'93''60'min'91'ys'93''8314'_636 :: T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_min'91'xs'93''60'min'91'ys'93''8314'_636 T_TotalOrder_652
v0
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min-mono-⊆
d_min'45'mono'45''8838'_646 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
d_min'45'mono'45''8838'_646 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
d_min'45'mono'45''8838'_646 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
  = T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_min'45'mono'45''8838'_646 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
du_min'45'mono'45''8838'_646 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
du_min'45'mono'45''8838'_646 :: T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_min'45'mono'45''8838'_646 T_TotalOrder_652
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4 AgdaAny
v5 AgdaAny -> T_Any_34 -> T_Any_34
v6
  = (T_TotalOrder_652
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_620 T_TotalOrder_652
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
      (([AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44)
-> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_tabulate_274 [AgdaAny]
v4
         (\ AgdaAny
v7 AgdaAny
v8 ->
            (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
              (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_Any_34 -> T_Any_34)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.du_map_76
                 (\ AgdaAny
v9 AgdaAny
v10 -> (T_TotalOrder_652 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652 -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_652 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
                 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ((AgdaAny -> T_Any_34 -> T_Any_34) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_34 -> T_Any_34
v6 AgdaAny
v7 AgdaAny
v8))))
-- Data.List.Extrema..extendedlambda0
d_'46'extendedlambda0_652 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda0_652 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
-> T_Any_34
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda0_652 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~[AgdaAny]
v6 ~[AgdaAny]
v7 ~AgdaAny
v8 ~AgdaAny -> T_Any_34 -> T_Any_34
v9
                          AgdaAny
v10 ~T_Any_34
v11 ~AgdaAny
v12 ~T__'8801'__12
v13
  = T_TotalOrder_652 -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_652 T_TotalOrder_652
v3 AgdaAny
v10
du_'46'extendedlambda0_652 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny
du_'46'extendedlambda0_652 :: T_TotalOrder_652 -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_652 T_TotalOrder_652
v0 AgdaAny
v1
  = let v2 :: T_IsTotalOrder_384
v2
          = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
              (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v3 :: T_IsPartialOrder_162
v3
             = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                 (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
            ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v3))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
-- Data.List.Extrema.max≤v⁺
d_max'8804'v'8314'_662 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_max'8804'v'8314'_662 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_max'8804'v'8314'_662 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_652
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_max'8804'v'8314'_662 T_TotalOrder_652
v3 AgdaAny
v5 [AgdaAny]
v6
du_max'8804'v'8314'_662 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_max'8804'v'8314'_662 :: T_TotalOrder_652
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_max'8804'v'8314'_662 T_TotalOrder_652
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_372 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.max<v⁺
d_max'60'v'8314'_672 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_max'60'v'8314'_672 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_max'60'v'8314'_672 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_652
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_max'60'v'8314'_672 T_TotalOrder_652
v3 AgdaAny
v5 [AgdaAny]
v6
du_max'60'v'8314'_672 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_max'60'v'8314'_672 :: T_TotalOrder_652
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_max'60'v'8314'_672 T_TotalOrder_652
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_382 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.v≤max⁺
d_v'8804'max'8314'_682 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_v'8804'max'8314'_682 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_v'8804'max'8314'_682 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4
  = T_TotalOrder_652
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_v'8804'max'8314'_682 T_TotalOrder_652
v3 AgdaAny
v4
du_v'8804'max'8314'_682 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_v'8804'max'8314'_682 :: T_TotalOrder_652
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_v'8804'max'8314'_682 T_TotalOrder_652
v0 AgdaAny
v1
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_352 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.v<max⁺
d_v'60'max'8314'_692 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'max'8314'_692 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_v'60'max'8314'_692 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4
  = T_TotalOrder_652
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_v'60'max'8314'_692 T_TotalOrder_652
v3 AgdaAny
v4
du_v'60'max'8314'_692 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'max'8314'_692 :: T_TotalOrder_652
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_v'60'max'8314'_692 T_TotalOrder_652
v0 AgdaAny
v1
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_362 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.⊥≤max
d_'8869''8804'max_698 ::
  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_TotalOrder_652 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_'8869''8804'max_698 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_'8869''8804'max_698 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_'8869''8804'max_698 T_TotalOrder_652
v3
du_'8869''8804'max_698 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_'8869''8804'max_698 :: T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_'8869''8804'max_698 T_TotalOrder_652
v0
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_388 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.xs≤max
d_xs'8804'max_706 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_xs'8804'max_706 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_xs'8804'max_706 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 = T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> T_All_44
du_xs'8804'max_706 T_TotalOrder_652
v3
du_xs'8804'max_706 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_xs'8804'max_706 :: T_TotalOrder_652 -> AgdaAny -> [AgdaAny] -> T_All_44
du_xs'8804'max_706 T_TotalOrder_652
v0
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_400 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.max≈v⁺
d_max'8776'v'8314'_716 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_max'8776'v'8314'_716 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_max'8776'v'8314'_716 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_max'8776'v'8314'_716 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
du_max'8776'v'8314'_716 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_max'8776'v'8314'_716 :: T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_max'8776'v'8314'_716 T_TotalOrder_652
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T_Any_34
 -> T_All_44
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_414 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
v4)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema.max[xs]≤max[ys]⁺
d_max'91'xs'93''8804'max'91'ys'93''8314'_732 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_max'91'xs'93''8804'max'91'ys'93''8314'_732 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_max'91'xs'93''8804'max'91'ys'93''8314'_732 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4
  = T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_732 T_TotalOrder_652
v3 AgdaAny
v4
du_max'91'xs'93''8804'max'91'ys'93''8314'_732 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_732 :: T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_732 T_TotalOrder_652
v0 AgdaAny
v1
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.max[xs]<max[ys]⁺
d_max'91'xs'93''60'max'91'ys'93''8314'_748 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_max'91'xs'93''60'max'91'ys'93''8314'_748 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_max'91'xs'93''60'max'91'ys'93''8314'_748 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4
  = T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_max'91'xs'93''60'max'91'ys'93''8314'_748 T_TotalOrder_652
v3 AgdaAny
v4
du_max'91'xs'93''60'max'91'ys'93''8314'_748 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_max'91'xs'93''60'max'91'ys'93''8314'_748 :: T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_max'91'xs'93''60'max'91'ys'93''8314'_748 T_TotalOrder_652
v0 AgdaAny
v1
  = (T_TotalOrder_652
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_652
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.max-mono-⊆
d_max'45'mono'45''8838'_758 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
d_max'45'mono'45''8838'_758 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
d_max'45'mono'45''8838'_758 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
  = T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_max'45'mono'45''8838'_758 T_TotalOrder_652
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
du_max'45'mono'45''8838'_758 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
du_max'45'mono'45''8838'_758 :: T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_max'45'mono'45''8838'_758 T_TotalOrder_652
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4 AgdaAny
v5 AgdaAny -> T_Any_34 -> T_Any_34
v6
  = (T_TotalOrder_652
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_732 T_TotalOrder_652
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
      (([AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44)
-> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_tabulate_274 [AgdaAny]
v3
         (\ AgdaAny
v7 AgdaAny
v8 ->
            (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
              (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_Any_34 -> T_Any_34)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.du_map_76
                 (\ AgdaAny
v9 AgdaAny
v10 -> (T_TotalOrder_652 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652 -> AgdaAny -> AgdaAny
du_'46'extendedlambda1_764 (T_TotalOrder_652 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_652
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
                 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ((AgdaAny -> T_Any_34 -> T_Any_34) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_34 -> T_Any_34
v6 AgdaAny
v7 AgdaAny
v8))))
-- Data.List.Extrema..extendedlambda1
d_'46'extendedlambda1_764 ::
  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_TotalOrder_652 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda1_764 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_652
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
-> T_Any_34
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda1_764 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_652
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~[AgdaAny]
v6 ~[AgdaAny]
v7 ~AgdaAny
v8 ~AgdaAny -> T_Any_34 -> T_Any_34
v9
                          AgdaAny
v10 ~T_Any_34
v11 ~AgdaAny
v12 ~T__'8801'__12
v13
  = T_TotalOrder_652 -> AgdaAny -> AgdaAny
du_'46'extendedlambda1_764 T_TotalOrder_652
v3 AgdaAny
v10
du_'46'extendedlambda1_764 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_652 ->
  AgdaAny -> AgdaAny
du_'46'extendedlambda1_764 :: T_TotalOrder_652 -> AgdaAny -> AgdaAny
du_'46'extendedlambda1_764 T_TotalOrder_652
v0 AgdaAny
v1
  = let v2 :: T_IsTotalOrder_384
v2
          = T_TotalOrder_652 -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_674
              (T_TotalOrder_652 -> T_TotalOrder_652
forall a b. a -> b
coe T_TotalOrder_652
v0) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (let v3 :: T_IsPartialOrder_162
v3
             = T_IsTotalOrder_384 -> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_392
                 (T_IsTotalOrder_384 -> T_IsTotalOrder_384
forall a b. a -> b
coe T_IsTotalOrder_384
v2) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         ((T_IsPreorder_70 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_98
            ((T_IsPartialOrder_162 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPartialOrder_162 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_170 (T_IsPartialOrder_162 -> AgdaAny
forall a b. a -> b
coe T_IsPartialOrder_162
v3))
            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))