{-# 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.Vec.Bounded.Base 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.Nat
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
import qualified MAlonzo.Code.Data.List.Membership.Setoid
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.Data.List.Relation.Unary.All.Properties
import qualified MAlonzo.Code.Data.List.Relation.Unary.Any
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Data.These.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Data.Vec.Bounded.Base._.argmax
d_argmax_10 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> Integer) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmax_10 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmax_10 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_argmax_144
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2
-- Data.Vec.Bounded.Base._.argmax-all
d_argmax'45'all_12 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> Integer) ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmax'45'all_12 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_argmax'45'all_12 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 AgdaAny -> Integer
v3 AgdaAny -> T_Level_18
v4 AgdaAny
v5 [AgdaAny]
v6 AgdaAny
v7 T_All_44
v8
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_argmax'45'all_518
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v3 AgdaAny
v5 [AgdaAny]
v6 AgdaAny
v7 T_All_44
v8
-- Data.Vec.Bounded.Base._.argmax-sel
d_argmax'45'sel_14 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmax'45'sel_14 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmax'45'sel_14 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.du_argmax'45'sel_506
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2
-- Data.Vec.Bounded.Base._.argmax[xs]<argmax[ys]⁺
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_16 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  (AgdaAny -> Integer) ->
  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'_16 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_16 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 AgdaAny -> Integer
v3 AgdaAny
v4 AgdaAny
v5
                                                [AgdaAny]
v6 [AgdaAny]
v7 T__'8846'__30
v8 T_All_44
v9
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> (AgdaAny -> Integer)
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_490
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny -> Integer
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 T__'8846'__30
v8 T_All_44
v9
-- Data.Vec.Bounded.Base._.argmax[xs]≤argmax[ys]⁺
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  (AgdaAny -> Integer) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_18 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_18 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 AgdaAny -> Integer
v3 AgdaAny
v4 AgdaAny
v5
                                                  [AgdaAny]
v6 [AgdaAny]
v7 T__'8846'__30
v8 T_All_44
v9
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_462
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny -> Integer
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 T__'8846'__30
v8 T_All_44
v9
-- Data.Vec.Bounded.Base._.argmin
d_argmin_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> Integer) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmin_20 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmin_20 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_argmin_140
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2
-- Data.Vec.Bounded.Base._.argmin-all
d_argmin'45'all_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> Integer) ->
  AgdaAny ->
  [AgdaAny] ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmin'45'all_22 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_All_44
-> AgdaAny
d_argmin'45'all_22 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 AgdaAny -> Integer
v3 AgdaAny
v4 [AgdaAny]
v5 AgdaAny -> T_Level_18
v6 AgdaAny
v7 T_All_44
v8
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_argmin'45'all_312
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v3 AgdaAny
v4 [AgdaAny]
v5 AgdaAny
v7 T_All_44
v8
-- Data.Vec.Bounded.Base._.argmin-sel
d_argmin'45'sel_24 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmin'45'sel_24 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmin'45'sel_24 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.du_argmin'45'sel_300
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2
-- Data.Vec.Bounded.Base._.argmin[xs]<argmin[ys]⁺
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  (AgdaAny -> Integer) ->
  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'_26 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_26 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 AgdaAny -> Integer
v3 AgdaAny
v4 AgdaAny
v5
                                                [AgdaAny]
v6 [AgdaAny]
v7 T__'8846'__30
v8 T_All_44
v9
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> (AgdaAny -> Integer)
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_284
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny -> Integer
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 T__'8846'__30
v8 T_All_44
v9
-- Data.Vec.Bounded.Base._.argmin[xs]≤argmin[ys]⁺
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_28 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  (AgdaAny -> Integer) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_28 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_28 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 AgdaAny -> Integer
v3 AgdaAny
v4 AgdaAny
v5
                                                  [AgdaAny]
v6 [AgdaAny]
v7 T__'8846'__30
v8 T_All_44
v9
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_256
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny -> Integer
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 T__'8846'__30
v8 T_All_44
v9
-- Data.Vec.Bounded.Base._.f[argmax]<v⁺
d_f'91'argmax'93''60'v'8314'_30 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  Integer ->
  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'_30 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_f'91'argmax'93''60'v'8314'_30 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 Integer
v3 AgdaAny
v4 [AgdaAny]
v5
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_f'91'argmax'93''60'v'8314'_404
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny
v4 [AgdaAny]
v5
-- Data.Vec.Bounded.Base._.f[argmax]≈f[v]⁺
d_f'91'argmax'93''8776'f'91'v'93''8314'_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_f'91'argmax'93''8776'f'91'v'93''8314'_32 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
d_f'91'argmax'93''8776'f'91'v'93''8314'_32 = T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.Vec.Bounded.Base._.f[argmax]≤v⁺
d_f'91'argmax'93''8804'v'8314'_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  Integer ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_f'91'argmax'93''8804'v'8314'_34 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
d_f'91'argmax'93''8804'v'8314'_34 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 Integer
v3 AgdaAny
v4 [AgdaAny]
v5
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_f'91'argmax'93''8804'v'8314'_394
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny
v4 [AgdaAny]
v5
-- Data.Vec.Bounded.Base._.f[argmin]<v⁺
d_f'91'argmin'93''60'v'8314'_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  Integer ->
  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'_36 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_f'91'argmin'93''60'v'8314'_36 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 Integer
v3
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_f'91'argmin'93''60'v'8314'_178
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 Integer
v3
-- Data.Vec.Bounded.Base._.f[argmin]≈f[v]⁺
d_f'91'argmin'93''8776'f'91'v'93''8314'_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_f'91'argmin'93''8776'f'91'v'93''8314'_38 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
d_f'91'argmin'93''8776'f'91'v'93''8314'_38 = T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.Vec.Bounded.Base._.f[argmin]≤f[xs]
d_f'91'argmin'93''8804'f'91'xs'93'_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_f'91'argmin'93''8804'f'91'xs'93'_40 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'argmin'93''8804'f'91'xs'93'_40 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 AgdaAny
v3 [AgdaAny]
v4
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
MAlonzo.Code.Data.List.Extrema.du_f'91'argmin'93''8804'f'91'xs'93'_216
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny
v3 [AgdaAny]
v4
-- Data.Vec.Bounded.Base._.f[argmin]≤f[⊤]
d_f'91'argmin'93''8804'f'91''8868''93'_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_f'91'argmin'93''8804'f'91''8868''93'_42 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
d_f'91'argmin'93''8804'f'91''8868''93'_42 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 AgdaAny
v3 [AgdaAny]
v4
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_f'91'argmin'93''8804'f'91''8868''93'_204
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny
v3 [AgdaAny]
v4
-- Data.Vec.Bounded.Base._.f[argmin]≤v⁺
d_f'91'argmin'93''8804'v'8314'_44 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  Integer ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_f'91'argmin'93''8804'v'8314'_44 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T__'8804'__22
d_f'91'argmin'93''8804'v'8314'_44 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 Integer
v3
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_f'91'argmin'93''8804'v'8314'_168
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 Integer
v3
-- Data.Vec.Bounded.Base._.f[xs]≤f[argmax]
d_f'91'xs'93''8804'f'91'argmax'93'_46 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_f'91'xs'93''8804'f'91'argmax'93'_46 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'xs'93''8804'f'91'argmax'93'_46 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 AgdaAny
v3 [AgdaAny]
v4
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
MAlonzo.Code.Data.List.Extrema.du_f'91'xs'93''8804'f'91'argmax'93'_422
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny
v3 [AgdaAny]
v4
-- Data.Vec.Bounded.Base._.f[⊥]≤f[argmax]
d_f'91''8869''93''8804'f'91'argmax'93'_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_f'91''8869''93''8804'f'91'argmax'93'_48 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
d_f'91''8869''93''8804'f'91'argmax'93'_48 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 AgdaAny
v3 [AgdaAny]
v4
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_f'91''8869''93''8804'f'91'argmax'93'_410
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny
v3 [AgdaAny]
v4
-- Data.Vec.Bounded.Base._.max
d_max_50 :: Integer -> [Integer] -> Integer
d_max_50 :: Integer -> [Integer] -> Integer
d_max_50
  = (T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> Integer -> [Integer] -> Integer
forall a b. a -> b
coe
      T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_max_150
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.max-mono-⊆
d_max'45'mono'45''8838'_52 ::
  Integer ->
  Integer ->
  [Integer] ->
  [Integer] ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  (Integer ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_max'45'mono'45''8838'_52 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8804'__22
-> (Integer -> T_Any_34 -> T_Any_34)
-> T__'8804'__22
d_max'45'mono'45''8838'_52
  = (T_TotalOrder_986
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> AgdaAny
 -> (AgdaAny -> T_Any_34 -> T_Any_34)
 -> AgdaAny)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8804'__22
-> (Integer -> T_Any_34 -> T_Any_34)
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_max'45'mono'45''8838'_780
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.max<v⁺
d_max'60'v'8314'_54 ::
  Integer ->
  Integer ->
  [Integer] ->
  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'_54 :: Integer -> Integer -> [Integer] -> T_Σ_14 -> T_All_44 -> T_Σ_14
d_max'60'v'8314'_54 Integer
v0 Integer
v1 [Integer]
v2
  = (T_TotalOrder_986
 -> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14)
-> AgdaAny -> Integer -> [Integer] -> T_Σ_14 -> T_All_44 -> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_max'60'v'8314'_694
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      Integer
v1 [Integer]
v2
-- Data.Vec.Bounded.Base._.max[xs]<max[ys]⁺
d_max'91'xs'93''60'max'91'ys'93''8314'_56 ::
  Integer ->
  Integer ->
  [Integer] ->
  [Integer] ->
  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'_56 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_max'91'xs'93''60'max'91'ys'93''8314'_56
  = (T_TotalOrder_986
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_max'91'xs'93''60'max'91'ys'93''8314'_770
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.max[xs]≤max[ys]⁺
d_max'91'xs'93''8804'max'91'ys'93''8314'_58 ::
  Integer ->
  Integer ->
  [Integer] ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_max'91'xs'93''8804'max'91'ys'93''8314'_58 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
d_max'91'xs'93''8804'max'91'ys'93''8314'_58
  = (T_TotalOrder_986
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_max'91'xs'93''8804'max'91'ys'93''8314'_754
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.max≈v⁺
d_max'8776'v'8314'_60 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_max'8776'v'8314'_60 :: Integer
-> Integer
-> [Integer]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
d_max'8776'v'8314'_60 = Integer
-> Integer
-> [Integer]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.Vec.Bounded.Base._.max≤v⁺
d_max'8804'v'8314'_62 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_max'8804'v'8314'_62 :: Integer
-> Integer
-> [Integer]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
d_max'8804'v'8314'_62 Integer
v0 Integer
v1 [Integer]
v2
  = (T_TotalOrder_986
 -> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny)
-> AgdaAny
-> Integer
-> [Integer]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_max'8804'v'8314'_684
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      Integer
v1 [Integer]
v2
-- Data.Vec.Bounded.Base._.min
d_min_64 :: Integer -> [Integer] -> Integer
d_min_64 :: Integer -> [Integer] -> Integer
d_min_64
  = (T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> Integer -> [Integer] -> Integer
forall a b. a -> b
coe
      T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_min_148
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.min-mono-⊆
d_min'45'mono'45''8838'_66 ::
  Integer ->
  Integer ->
  [Integer] ->
  [Integer] ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  (Integer ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_min'45'mono'45''8838'_66 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8804'__22
-> (Integer -> T_Any_34 -> T_Any_34)
-> T__'8804'__22
d_min'45'mono'45''8838'_66
  = (T_TotalOrder_986
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> AgdaAny
 -> (AgdaAny -> T_Any_34 -> T_Any_34)
 -> AgdaAny)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8804'__22
-> (Integer -> T_Any_34 -> T_Any_34)
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_min'45'mono'45''8838'_668
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.min<v⁺
d_min'60'v'8314'_68 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_min'60'v'8314'_68 :: Integer -> Integer -> [Integer] -> T__'8846'__30 -> T_Σ_14
d_min'60'v'8314'_68
  = (T_TotalOrder_986
 -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_min'60'v'8314'_582
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.min[xs]<min[ys]⁺
d_min'91'xs'93''60'min'91'ys'93''8314'_70 ::
  Integer ->
  Integer ->
  [Integer] ->
  [Integer] ->
  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'_70 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_min'91'xs'93''60'min'91'ys'93''8314'_70
  = (T_TotalOrder_986
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_min'91'xs'93''60'min'91'ys'93''8314'_658
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.min[xs]≤min[ys]⁺
d_min'91'xs'93''8804'min'91'ys'93''8314'_72 ::
  Integer ->
  Integer ->
  [Integer] ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_min'91'xs'93''8804'min'91'ys'93''8314'_72 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
d_min'91'xs'93''8804'min'91'ys'93''8314'_72
  = (T_TotalOrder_986
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_min'91'xs'93''8804'min'91'ys'93''8314'_642
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.min≈v⁺
d_min'8776'v'8314'_74 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_min'8776'v'8314'_74 :: Integer
-> Integer
-> [Integer]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
d_min'8776'v'8314'_74 = Integer
-> Integer
-> [Integer]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.Vec.Bounded.Base._.min≤v⁺
d_min'8804'v'8314'_76 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_min'8804'v'8314'_76 :: Integer -> Integer -> [Integer] -> T__'8846'__30 -> T__'8804'__22
d_min'8804'v'8314'_76
  = (T_TotalOrder_986
 -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> T__'8846'__30
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_min'8804'v'8314'_572
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.min≤xs
d_min'8804'xs_78 ::
  Integer ->
  [Integer] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_min'8804'xs_78 :: Integer -> [Integer] -> T_All_44
d_min'8804'xs_78
  = (T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny -> Integer -> [Integer] -> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44
MAlonzo.Code.Data.List.Extrema.du_min'8804'xs_616
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.min≤⊤
d_min'8804''8868'_80 ::
  Integer -> [Integer] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_min'8804''8868'_80 :: Integer -> [Integer] -> T__'8804'__22
d_min'8804''8868'_80
  = (T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> Integer -> [Integer] -> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_min'8804''8868'_608
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.v<f[argmax]⁺
d_v'60'f'91'argmax'93''8314'_82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  Integer ->
  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'_82 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_v'60'f'91'argmax'93''8314'_82 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 Integer
v3
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_v'60'f'91'argmax'93''8314'_384
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 Integer
v3
-- Data.Vec.Bounded.Base._.v<f[argmin]⁺
d_v'60'f'91'argmin'93''8314'_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  Integer ->
  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'_84 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_v'60'f'91'argmin'93''8314'_84 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 Integer
v3 AgdaAny
v4 [AgdaAny]
v5
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_v'60'f'91'argmin'93''8314'_198
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny
v4 [AgdaAny]
v5
-- Data.Vec.Bounded.Base._.v<max⁺
d_v'60'max'8314'_86 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'max'8314'_86 :: Integer -> Integer -> [Integer] -> T__'8846'__30 -> T_Σ_14
d_v'60'max'8314'_86
  = (T_TotalOrder_986
 -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_v'60'max'8314'_714
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.v<min⁺
d_v'60'min'8314'_88 ::
  Integer ->
  Integer ->
  [Integer] ->
  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'_88 :: Integer -> Integer -> [Integer] -> T_Σ_14 -> T_All_44 -> T_Σ_14
d_v'60'min'8314'_88 Integer
v0 Integer
v1 [Integer]
v2
  = (T_TotalOrder_986
 -> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14)
-> AgdaAny -> Integer -> [Integer] -> T_Σ_14 -> T_All_44 -> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
MAlonzo.Code.Data.List.Extrema.du_v'60'min'8314'_602
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      Integer
v1 [Integer]
v2
-- Data.Vec.Bounded.Base._.v≤f[argmax]⁺
d_v'8804'f'91'argmax'93''8314'_90 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  Integer ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_v'8804'f'91'argmax'93''8314'_90 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T__'8804'__22
d_v'8804'f'91'argmax'93''8314'_90 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 Integer
v3
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_v'8804'f'91'argmax'93''8314'_374
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 Integer
v3
-- Data.Vec.Bounded.Base._.v≤f[argmin]⁺
d_v'8804'f'91'argmin'93''8314'_92 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  Integer ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_v'8804'f'91'argmin'93''8314'_92 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
d_v'8804'f'91'argmin'93''8314'_92 T_Level_18
v0 T_Level_18
v1 AgdaAny -> Integer
v2 Integer
v3 AgdaAny
v4 [AgdaAny]
v5
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_v'8804'f'91'argmin'93''8314'_188
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      AgdaAny -> Integer
v2 AgdaAny
v4 [AgdaAny]
v5
-- Data.Vec.Bounded.Base._.v≤max⁺
d_v'8804'max'8314'_94 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_v'8804'max'8314'_94 :: Integer -> Integer -> [Integer] -> T__'8846'__30 -> T__'8804'__22
d_v'8804'max'8314'_94
  = (T_TotalOrder_986
 -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> Integer
-> Integer
-> [Integer]
-> T__'8846'__30
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_v'8804'max'8314'_704
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.v≤min⁺
d_v'8804'min'8314'_96 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_v'8804'min'8314'_96 :: Integer
-> Integer
-> [Integer]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
d_v'8804'min'8314'_96 Integer
v0 Integer
v1 [Integer]
v2
  = (T_TotalOrder_986
 -> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny)
-> AgdaAny
-> Integer
-> [Integer]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_v'8804'min'8314'_592
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
      Integer
v1 [Integer]
v2
-- Data.Vec.Bounded.Base._.xs≤max
d_xs'8804'max_98 ::
  Integer ->
  [Integer] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_xs'8804'max_98 :: Integer -> [Integer] -> T_All_44
d_xs'8804'max_98
  = (T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny -> Integer -> [Integer] -> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44
MAlonzo.Code.Data.List.Extrema.du_xs'8804'max_728
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base._.⊥≤max
d_'8869''8804'max_100 ::
  Integer -> [Integer] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'8869''8804'max_100 :: Integer -> [Integer] -> T__'8804'__22
d_'8869''8804'max_100
  = (T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> Integer -> [Integer] -> T__'8804'__22
forall a b. a -> b
coe
      T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_'8869''8804'max_720
      (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966)
-- Data.Vec.Bounded.Base.Vec≤
d_Vec'8804'_126 :: p -> p -> p -> T_Level_18
d_Vec'8804'_126 p
a0 p
a1 p
a2 = ()
data T_Vec'8804'_126
  = C__'44'__144 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_28
-- Data.Vec.Bounded.Base.Vec≤.length
d_length_138 :: T_Vec'8804'_126 -> Integer
d_length_138 :: T_Vec'8804'_126 -> Integer
d_length_138 T_Vec'8804'_126
v0
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v0 of
      C__'44'__144 Integer
v1 T_Vec_28
v2 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      T_Vec'8804'_126
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.Vec≤.vec
d_vec_140 :: T_Vec'8804'_126 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_vec_140 :: T_Vec'8804'_126 -> T_Vec_28
d_vec_140 T_Vec'8804'_126
v0
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v0 of
      C__'44'__144 Integer
v1 T_Vec_28
v2 -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2
      T_Vec'8804'_126
_ -> T_Vec_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.isBounded
d_isBounded_148 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  T_Vec'8804'_126 -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_isBounded_148 :: T_Level_18
-> T_Level_18 -> Integer -> T_Vec'8804'_126 -> T__'8804'__22
d_isBounded_148 ~T_Level_18
v0 ~T_Level_18
v1 Integer
v2 T_Vec'8804'_126
v3 = Integer -> T_Vec'8804'_126 -> T__'8804'__22
du_isBounded_148 Integer
v2 T_Vec'8804'_126
v3
du_isBounded_148 ::
  Integer ->
  T_Vec'8804'_126 -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
du_isBounded_148 :: Integer -> T_Vec'8804'_126 -> T__'8804'__22
du_isBounded_148 Integer
v0 T_Vec'8804'_126
v1
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v1 of
      C__'44'__144 Integer
v2 T_Vec_28
v3
        -> (T_Dec_20 -> AgdaAny -> AgdaAny)
-> T_Dec_20 -> AgdaAny -> T__'8804'__22
forall a b. a -> b
coe
             T_Dec_20 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_recompute_54
             (Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8804''63'__2920
                (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
             AgdaAny
forall a. a
erased
      T_Vec'8804'_126
_ -> T__'8804'__22
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.toVec
d_toVec_156 ::
  T_Vec'8804'_126 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_toVec_156 :: T_Vec'8804'_126 -> T_Vec_28
d_toVec_156 T_Vec'8804'_126
v0
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v0 of
      C__'44'__144 Integer
v1 T_Vec_28
v2 -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2
      T_Vec'8804'_126
_ -> T_Vec_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.fromVec
d_fromVec_162 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> T_Vec'8804'_126
d_fromVec_162 :: T_Level_18 -> T_Level_18 -> Integer -> T_Vec_28 -> T_Vec'8804'_126
d_fromVec_162 ~T_Level_18
v0 ~T_Level_18
v1 Integer
v2 T_Vec_28
v3 = Integer -> T_Vec_28 -> T_Vec'8804'_126
du_fromVec_162 Integer
v2 T_Vec_28
v3
du_fromVec_162 ::
  Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> T_Vec'8804'_126
du_fromVec_162 :: Integer -> T_Vec_28 -> T_Vec'8804'_126
du_fromVec_162 Integer
v0 T_Vec_28
v1 = (Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> T_Vec_28 -> T_Vec'8804'_126
forall a b. a -> b
coe Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144 Integer
v0 T_Vec_28
v1
-- Data.Vec.Bounded.Base.padRight
d_padRight_166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  AgdaAny -> T_Vec'8804'_126 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_padRight_166 :: T_Level_18
-> T_Level_18 -> Integer -> AgdaAny -> T_Vec'8804'_126 -> T_Vec_28
d_padRight_166 ~T_Level_18
v0 ~T_Level_18
v1 Integer
v2 AgdaAny
v3 T_Vec'8804'_126
v4 = Integer -> AgdaAny -> T_Vec'8804'_126 -> T_Vec_28
du_padRight_166 Integer
v2 AgdaAny
v3 T_Vec'8804'_126
v4
du_padRight_166 ::
  Integer ->
  AgdaAny -> T_Vec'8804'_126 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28
du_padRight_166 :: Integer -> AgdaAny -> T_Vec'8804'_126 -> T_Vec_28
du_padRight_166 Integer
v0 AgdaAny
v1 T_Vec'8804'_126
v2
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v2 of
      C__'44'__144 Integer
v3 T_Vec_28
v4
        -> let v6 :: AgdaAny
v6 = (Integer -> Integer -> Integer) -> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 Integer
v3 in
           AgdaAny -> T_Vec_28
forall a b. a -> b
coe
             ((T_Vec_28 -> T_Vec_28 -> T_Vec_28) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Vec_28 -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du__'43''43'__188 (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v4)
                ((Integer -> AgdaAny -> T_Vec_28) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Integer -> AgdaAny -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
      T_Vec'8804'_126
_ -> T_Vec_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.padLeft
d_padLeft_182 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  AgdaAny -> T_Vec'8804'_126 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_padLeft_182 :: T_Level_18
-> T_Level_18 -> Integer -> AgdaAny -> T_Vec'8804'_126 -> T_Vec_28
d_padLeft_182 ~T_Level_18
v0 ~T_Level_18
v1 Integer
v2 AgdaAny
v3 T_Vec'8804'_126
v4 = Integer -> AgdaAny -> T_Vec'8804'_126 -> T_Vec_28
du_padLeft_182 Integer
v2 AgdaAny
v3 T_Vec'8804'_126
v4
du_padLeft_182 ::
  Integer ->
  AgdaAny -> T_Vec'8804'_126 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28
du_padLeft_182 :: Integer -> AgdaAny -> T_Vec'8804'_126 -> T_Vec_28
du_padLeft_182 Integer
v0 AgdaAny
v1 T_Vec'8804'_126
v2
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v2 of
      C__'44'__144 Integer
v3 T_Vec_28
v4
        -> let v6 :: AgdaAny
v6 = (Integer -> Integer -> Integer) -> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 Integer
v3 in
           AgdaAny -> T_Vec_28
forall a b. a -> b
coe
             ((T_Vec_28 -> T_Vec_28 -> T_Vec_28) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Vec_28 -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du__'43''43'__188
                ((Integer -> AgdaAny -> T_Vec_28) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> AgdaAny -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v4))
      T_Vec'8804'_126
_ -> T_Vec_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.split
d_split_206 ::
  Integer ->
  Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_split_206 :: Integer -> Integer -> T__'8801'__12
d_split_206 = Integer -> Integer -> T__'8801'__12
forall a. a
erased
-- Data.Vec.Bounded.Base.padBoth
d_padBoth_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  AgdaAny ->
  AgdaAny -> T_Vec'8804'_126 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_padBoth_220 :: T_Level_18
-> T_Level_18
-> Integer
-> AgdaAny
-> AgdaAny
-> T_Vec'8804'_126
-> T_Vec_28
d_padBoth_220 ~T_Level_18
v0 ~T_Level_18
v1 Integer
v2 AgdaAny
v3 AgdaAny
v4 T_Vec'8804'_126
v5 = Integer -> AgdaAny -> AgdaAny -> T_Vec'8804'_126 -> T_Vec_28
du_padBoth_220 Integer
v2 AgdaAny
v3 AgdaAny
v4 T_Vec'8804'_126
v5
du_padBoth_220 ::
  Integer ->
  AgdaAny ->
  AgdaAny -> T_Vec'8804'_126 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28
du_padBoth_220 :: Integer -> AgdaAny -> AgdaAny -> T_Vec'8804'_126 -> T_Vec_28
du_padBoth_220 Integer
v0 AgdaAny
v1 AgdaAny
v2 T_Vec'8804'_126
v3
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v3 of
      C__'44'__144 Integer
v4 T_Vec_28
v5
        -> let v7 :: AgdaAny
v7 = (Integer -> Integer -> Integer) -> Integer -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v0 Integer
v4 in
           AgdaAny -> T_Vec_28
forall a b. a -> b
coe
             ((T_Vec_28 -> T_Vec_28 -> T_Vec_28) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Vec_28 -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du__'43''43'__188
                ((Integer -> AgdaAny -> T_Vec_28) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Integer -> AgdaAny -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444
                   ((Integer -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_'8970'_'47'2'8971'_268 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                ((T_Vec_28 -> T_Vec_28 -> T_Vec_28) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Vec_28 -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du__'43''43'__188 (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v5)
                   ((Integer -> AgdaAny -> T_Vec_28) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      Integer -> AgdaAny -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444
                      ((Integer -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_'8968'_'47'2'8969'_272 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
                      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
      T_Vec'8804'_126
_ -> T_Vec_28
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.fromList
d_fromList_244 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> [AgdaAny] -> T_Vec'8804'_126
d_fromList_244 :: T_Level_18 -> T_Level_18 -> [AgdaAny] -> T_Vec'8804'_126
d_fromList_244 ~T_Level_18
v0 ~T_Level_18
v1 [AgdaAny]
v2 = [AgdaAny] -> T_Vec'8804'_126
du_fromList_244 [AgdaAny]
v2
du_fromList_244 :: [AgdaAny] -> T_Vec'8804'_126
du_fromList_244 :: [AgdaAny] -> T_Vec'8804'_126
du_fromList_244 [AgdaAny]
v0
  = (Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> AgdaAny -> AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
      Integer -> T_Vec_28 -> T_Vec'8804'_126
du_fromVec_162 (([AgdaAny] -> Integer) -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> Integer
MAlonzo.Code.Data.List.Base.du_length_268 [AgdaAny]
v0)
      (([AgdaAny] -> T_Vec_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_fromList_600 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0))
-- Data.Vec.Bounded.Base.toList
d_toList_246 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Integer -> T_Vec'8804'_126 -> [AgdaAny]
d_toList_246 :: T_Level_18 -> T_Level_18 -> Integer -> T_Vec'8804'_126 -> [AgdaAny]
d_toList_246 ~T_Level_18
v0 ~T_Level_18
v1 ~Integer
v2 T_Vec'8804'_126
v3 = T_Vec'8804'_126 -> [AgdaAny]
du_toList_246 T_Vec'8804'_126
v3
du_toList_246 :: T_Vec'8804'_126 -> [AgdaAny]
du_toList_246 :: T_Vec'8804'_126 -> [AgdaAny]
du_toList_246 T_Vec'8804'_126
v0
  = (T_Vec_28 -> [AgdaAny]) -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
      T_Vec_28 -> [AgdaAny]
MAlonzo.Code.Data.Vec.Base.du_toList_592 ((T_Vec'8804'_126 -> T_Vec_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Vec'8804'_126 -> T_Vec_28
d_vec_140 (T_Vec'8804'_126 -> AgdaAny
forall a b. a -> b
coe T_Vec'8804'_126
v0))
-- Data.Vec.Bounded.Base.replicate
d_replicate_250 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  AgdaAny -> T_Vec'8804'_126
d_replicate_250 :: Integer
-> Integer
-> T_Level_18
-> T_Level_18
-> T__'8804'__22
-> AgdaAny
-> T_Vec'8804'_126
d_replicate_250 Integer
v0 ~Integer
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T__'8804'__22
v4 AgdaAny
v5 = Integer -> AgdaAny -> T_Vec'8804'_126
du_replicate_250 Integer
v0 AgdaAny
v5
du_replicate_250 :: Integer -> AgdaAny -> T_Vec'8804'_126
du_replicate_250 :: Integer -> AgdaAny -> T_Vec'8804'_126
du_replicate_250 Integer
v0 AgdaAny
v1
  = (Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
      Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144 Integer
v0
      ((Integer -> AgdaAny -> T_Vec_28) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> AgdaAny -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
-- Data.Vec.Bounded.Base.[]
d_'91''93'_256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Integer -> T_Vec'8804'_126
d_'91''93'_256 :: T_Level_18 -> T_Level_18 -> Integer -> T_Vec'8804'_126
d_'91''93'_256 ~T_Level_18
v0 ~T_Level_18
v1 ~Integer
v2 = T_Vec'8804'_126
du_'91''93'_256
du_'91''93'_256 :: T_Vec'8804'_126
du_'91''93'_256 :: T_Vec'8804'_126
du_'91''93'_256
  = (Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
      Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144 (Integer
0 :: Integer)
      (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32)
-- Data.Vec.Bounded.Base._∷_
d__'8759'__258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Integer -> AgdaAny -> T_Vec'8804'_126 -> T_Vec'8804'_126
d__'8759'__258 :: T_Level_18
-> T_Level_18
-> Integer
-> AgdaAny
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d__'8759'__258 ~T_Level_18
v0 ~T_Level_18
v1 ~Integer
v2 AgdaAny
v3 T_Vec'8804'_126
v4 = AgdaAny -> T_Vec'8804'_126 -> T_Vec'8804'_126
du__'8759'__258 AgdaAny
v3 T_Vec'8804'_126
v4
du__'8759'__258 :: AgdaAny -> T_Vec'8804'_126 -> T_Vec'8804'_126
du__'8759'__258 :: AgdaAny -> T_Vec'8804'_126 -> T_Vec'8804'_126
du__'8759'__258 AgdaAny
v0 T_Vec'8804'_126
v1
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v1 of
      C__'44'__144 Integer
v2 T_Vec_28
v3
        -> (Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
             Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v2))
             ((AgdaAny -> T_Vec_28 -> T_Vec_28) -> AgdaAny -> T_Vec_28 -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 AgdaAny
v0 T_Vec_28
v3)
      T_Vec'8804'_126
_ -> T_Vec'8804'_126
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.≤-cast
d_'8804''45'cast_268 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
  T_Vec'8804'_126 -> T_Vec'8804'_126
d_'8804''45'cast_268 :: Integer
-> Integer
-> T_Level_18
-> T_Level_18
-> T__'8804'__22
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d_'8804''45'cast_268 ~Integer
v0 ~Integer
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T__'8804'__22
v4 T_Vec'8804'_126
v5
  = T_Vec'8804'_126 -> T_Vec'8804'_126
du_'8804''45'cast_268 T_Vec'8804'_126
v5
du_'8804''45'cast_268 :: T_Vec'8804'_126 -> T_Vec'8804'_126
du_'8804''45'cast_268 :: T_Vec'8804'_126 -> T_Vec'8804'_126
du_'8804''45'cast_268 T_Vec'8804'_126
v0 = T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v0
-- Data.Vec.Bounded.Base.≡-cast
d_'8801''45'cast_278 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T_Vec'8804'_126 -> T_Vec'8804'_126
d_'8801''45'cast_278 :: Integer
-> Integer
-> T_Level_18
-> T_Level_18
-> T__'8801'__12
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d_'8801''45'cast_278 ~Integer
v0 ~Integer
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T__'8801'__12
v4 T_Vec'8804'_126
v5
  = T_Vec'8804'_126 -> T_Vec'8804'_126
du_'8801''45'cast_278 T_Vec'8804'_126
v5
du_'8801''45'cast_278 :: T_Vec'8804'_126 -> T_Vec'8804'_126
du_'8801''45'cast_278 :: T_Vec'8804'_126 -> T_Vec'8804'_126
du_'8801''45'cast_278 T_Vec'8804'_126
v0 = T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v0
-- Data.Vec.Bounded.Base.map
d_map_282 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  (AgdaAny -> AgdaAny) -> T_Vec'8804'_126 -> T_Vec'8804'_126
d_map_282 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Integer
-> (AgdaAny -> AgdaAny)
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d_map_282 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~Integer
v4 AgdaAny -> AgdaAny
v5 T_Vec'8804'_126
v6 = (AgdaAny -> AgdaAny) -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_map_282 AgdaAny -> AgdaAny
v5 T_Vec'8804'_126
v6
du_map_282 ::
  (AgdaAny -> AgdaAny) -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_map_282 :: (AgdaAny -> AgdaAny) -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_map_282 AgdaAny -> AgdaAny
v0 T_Vec'8804'_126
v1
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v1 of
      C__'44'__144 Integer
v2 T_Vec_28
v3
        -> (Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
             Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144 Integer
v2
             (((AgdaAny -> AgdaAny) -> T_Vec_28 -> T_Vec_28)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_map_178 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v3))
      T_Vec'8804'_126
_ -> T_Vec'8804'_126
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.reverse
d_reverse_290 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
d_reverse_290 :: T_Level_18
-> T_Level_18 -> Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
d_reverse_290 ~T_Level_18
v0 ~T_Level_18
v1 ~Integer
v2 T_Vec'8804'_126
v3 = T_Vec'8804'_126 -> T_Vec'8804'_126
du_reverse_290 T_Vec'8804'_126
v3
du_reverse_290 :: T_Vec'8804'_126 -> T_Vec'8804'_126
du_reverse_290 :: T_Vec'8804'_126 -> T_Vec'8804'_126
du_reverse_290 T_Vec'8804'_126
v0
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v0 of
      C__'44'__144 Integer
v1 T_Vec_28
v2
        -> (Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
             Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144 Integer
v1 ((T_Vec_28 -> T_Vec_28) -> T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_reverse_616 T_Vec_28
v2)
      T_Vec'8804'_126
_ -> T_Vec'8804'_126
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.alignWith
d_alignWith_296 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
  T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
d_alignWith_296 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Integer
-> (T_These_38 -> AgdaAny)
-> T_Vec'8804'_126
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d_alignWith_296 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~Integer
v6 T_These_38 -> AgdaAny
v7 T_Vec'8804'_126
v8 T_Vec'8804'_126
v9
  = (T_These_38 -> AgdaAny)
-> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_alignWith_296 T_These_38 -> AgdaAny
v7 T_Vec'8804'_126
v8 T_Vec'8804'_126
v9
du_alignWith_296 ::
  (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
  T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_alignWith_296 :: (T_These_38 -> AgdaAny)
-> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_alignWith_296 T_These_38 -> AgdaAny
v0 T_Vec'8804'_126
v1 T_Vec'8804'_126
v2
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v1 of
      C__'44'__144 Integer
v3 T_Vec_28
v4
        -> case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v2 of
             C__'44'__144 Integer
v6 T_Vec_28
v7
               -> (Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
                    Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144
                    (Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8852'__208 (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe Integer
v6))
                    (((T_These_38 -> AgdaAny) -> T_Vec_28 -> T_Vec_28 -> T_Vec_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (T_These_38 -> AgdaAny) -> T_Vec_28 -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_alignWith_204 ((T_These_38 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_These_38 -> AgdaAny
v0) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v4)
                       (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v7))
             T_Vec'8804'_126
_ -> T_Vec'8804'_126
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Vec'8804'_126
_ -> T_Vec'8804'_126
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.zipWith
d_zipWith_308 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
d_zipWith_308 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Integer
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Vec'8804'_126
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d_zipWith_308 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~Integer
v6 AgdaAny -> AgdaAny -> AgdaAny
v7 T_Vec'8804'_126
v8 T_Vec'8804'_126
v9
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_zipWith_308 AgdaAny -> AgdaAny -> AgdaAny
v7 T_Vec'8804'_126
v8 T_Vec'8804'_126
v9
du_zipWith_308 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_zipWith_308 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_zipWith_308 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Vec'8804'_126
v1 T_Vec'8804'_126
v2
  = case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v1 of
      C__'44'__144 Integer
v3 T_Vec_28
v4
        -> case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v2 of
             C__'44'__144 Integer
v6 T_Vec_28
v7
               -> (Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
                    Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144
                    (Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8851'__236 (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe Integer
v6))
                    (((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Vec_28 -> T_Vec_28 -> T_Vec_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (AgdaAny -> AgdaAny -> AgdaAny) -> T_Vec_28 -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_restrictWith_224 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v4)
                       (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v7))
             T_Vec'8804'_126
_ -> T_Vec'8804'_126
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Vec'8804'_126
_ -> T_Vec'8804'_126
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Vec.Bounded.Base.zip
d_zip_320 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
d_zip_320 :: T_Level_18
-> T_Level_18
-> Integer
-> T_Level_18
-> T_Level_18
-> T_Vec'8804'_126
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d_zip_320 ~T_Level_18
v0 ~T_Level_18
v1 ~Integer
v2 ~T_Level_18
v3 ~T_Level_18
v4 = T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_zip_320
du_zip_320 :: T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_zip_320 :: T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_zip_320
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126)
-> AgdaAny -> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_zipWith_308 ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32)
-- Data.Vec.Bounded.Base.align
d_align_322 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Integer ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
d_align_322 :: T_Level_18
-> T_Level_18
-> Integer
-> T_Level_18
-> T_Level_18
-> T_Vec'8804'_126
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d_align_322 ~T_Level_18
v0 ~T_Level_18
v1 ~Integer
v2 ~T_Level_18
v3 ~T_Level_18
v4 = T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_align_322
du_align_322 ::
  T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_align_322 :: T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_align_322 = ((T_These_38 -> AgdaAny)
 -> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126)
-> AgdaAny -> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe (T_These_38 -> AgdaAny)
-> T_Vec'8804'_126 -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_alignWith_296 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> AgdaAny
v0))
-- Data.Vec.Bounded.Base.take
d_take_326 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Integer -> Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
d_take_326 :: T_Level_18
-> T_Level_18
-> Integer
-> Integer
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d_take_326 ~T_Level_18
v0 ~T_Level_18
v1 ~Integer
v2 Integer
v3 T_Vec'8804'_126
v4 = Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_take_326 Integer
v3 T_Vec'8804'_126
v4
du_take_326 :: Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_take_326 :: Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_take_326 Integer
v0 T_Vec'8804'_126
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
du_'91''93'_256
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
             (case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v1 of
                C__'44'__144 Integer
v3 T_Vec_28
v4
                  -> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v4 of
                       T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32 -> T_Vec'8804'_126 -> AgdaAny
forall a b. a -> b
coe T_Vec'8804'_126
du_'91''93'_256
                       MAlonzo.Code.Data.Vec.Base.C__'8759'__38 AgdaAny
v7 T_Vec_28
v8
                         -> let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              ((AgdaAny -> T_Vec'8804'_126 -> T_Vec'8804'_126)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> T_Vec'8804'_126 -> T_Vec'8804'_126
du__'8759'__258 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)
                                 ((Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_take_326 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) ((Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> T_Vec_28 -> AgdaAny
forall a b. a -> b
coe Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144 Integer
v9 T_Vec_28
v8)))
                       T_Vec_28
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_Vec'8804'_126
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Vec.Bounded.Base.drop
d_drop_344 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> Integer -> Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
d_drop_344 :: T_Level_18
-> T_Level_18
-> Integer
-> Integer
-> T_Vec'8804'_126
-> T_Vec'8804'_126
d_drop_344 ~T_Level_18
v0 ~T_Level_18
v1 ~Integer
v2 Integer
v3 T_Vec'8804'_126
v4 = Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_drop_344 Integer
v3 T_Vec'8804'_126
v4
du_drop_344 :: Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_drop_344 :: Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_drop_344 Integer
v0 T_Vec'8804'_126
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Vec'8804'_126
forall a b. a -> b
coe
             (case T_Vec'8804'_126 -> T_Vec'8804'_126
forall a b. a -> b
coe T_Vec'8804'_126
v1 of
                C__'44'__144 Integer
v3 T_Vec_28
v4
                  -> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v4 of
                       T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32 -> T_Vec'8804'_126 -> AgdaAny
forall a b. a -> b
coe T_Vec'8804'_126
du_'91''93'_256
                       MAlonzo.Code.Data.Vec.Base.C__'8759'__38 AgdaAny
v7 T_Vec_28
v8
                         -> let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe ((Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T_Vec'8804'_126 -> T_Vec'8804'_126
du_drop_344 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) ((Integer -> T_Vec_28 -> T_Vec'8804'_126)
-> Integer -> T_Vec_28 -> AgdaAny
forall a b. a -> b
coe Integer -> T_Vec_28 -> T_Vec'8804'_126
C__'44'__144 Integer
v9 T_Vec_28
v8))
                       T_Vec_28
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_Vec'8804'_126
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Vec.Bounded.Base.rectangle
d_rectangle_362 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_rectangle_362 :: T_Level_18 -> T_Level_18 -> [T_Σ_14] -> T_Σ_14
d_rectangle_362 ~T_Level_18
v0 ~T_Level_18
v1 [T_Σ_14]
v2 = [T_Σ_14] -> T_Σ_14
du_rectangle_362 [T_Σ_14]
v2
du_rectangle_362 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_rectangle_362 :: [T_Σ_14] -> T_Σ_14
du_rectangle_362 [T_Σ_14]
v0
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (([T_Σ_14] -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Σ_14] -> Integer
du_width_374 ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v0)) (([T_Σ_14] -> [T_Vec'8804'_126]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Σ_14] -> [T_Vec'8804'_126]
du_padded_380 ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v0))
-- Data.Vec.Bounded.Base._.sizes
d_sizes_372 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> [Integer]
d_sizes_372 :: T_Level_18 -> T_Level_18 -> [T_Σ_14] -> [Integer]
d_sizes_372 ~T_Level_18
v0 ~T_Level_18
v1 [T_Σ_14]
v2 = [T_Σ_14] -> [Integer]
du_sizes_372 [T_Σ_14]
v2
du_sizes_372 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> [Integer]
du_sizes_372 :: [T_Σ_14] -> [Integer]
du_sizes_372 [T_Σ_14]
v0
  = ((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [Integer]
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v1)))
      ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v0)
-- Data.Vec.Bounded.Base._.width
d_width_374 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> Integer
d_width_374 :: T_Level_18 -> T_Level_18 -> [T_Σ_14] -> Integer
d_width_374 ~T_Level_18
v0 ~T_Level_18
v1 [T_Σ_14]
v2 = [T_Σ_14] -> Integer
du_width_374 [T_Σ_14]
v2
du_width_374 :: [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> Integer
du_width_374 :: [T_Σ_14] -> Integer
du_width_374 [T_Σ_14]
v0
  = (T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_986 -> Integer -> AgdaAny -> Integer
forall a b. a -> b
coe
      T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Extrema.du_max_150
      T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966
      (Integer
0 :: Integer) (([T_Σ_14] -> [Integer]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Σ_14] -> [Integer]
du_sizes_372 ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v0))
-- Data.Vec.Bounded.Base._.all≤
d_all'8804'_378 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_all'8804'_378 :: T_Level_18 -> T_Level_18 -> [T_Σ_14] -> T_All_44
d_all'8804'_378 ~T_Level_18
v0 ~T_Level_18
v1 [T_Σ_14]
v2 = [T_Σ_14] -> T_All_44
du_all'8804'_378 [T_Σ_14]
v2
du_all'8804'_378 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_all'8804'_378 :: [T_Σ_14] -> T_All_44
du_all'8804'_378 [T_Σ_14]
v0
  = ([AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
      [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.Properties.du_map'8315'_504
      ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v0)
      ((T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44)
-> T_TotalOrder_986 -> Integer -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44
MAlonzo.Code.Data.List.Extrema.du_xs'8804'max_728
         T_TotalOrder_986
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2966
         (Integer
0 :: Integer) (([T_Σ_14] -> [Integer]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Σ_14] -> [Integer]
du_sizes_372 ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v0)))
-- Data.Vec.Bounded.Base._.padded
d_padded_380 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> [T_Vec'8804'_126]
d_padded_380 :: T_Level_18 -> T_Level_18 -> [T_Σ_14] -> [T_Vec'8804'_126]
d_padded_380 ~T_Level_18
v0 ~T_Level_18
v1 [T_Σ_14]
v2 = [T_Σ_14] -> [T_Vec'8804'_126]
du_padded_380 [T_Σ_14]
v2
du_padded_380 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] -> [T_Vec'8804'_126]
du_padded_380 :: [T_Σ_14] -> [T_Vec'8804'_126]
du_padded_380 [T_Σ_14]
v0
  = (T_Setoid_46
 -> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny -> [T_Vec'8804'_126]
forall a b. a -> b
coe
      T_Setoid_46
-> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny]
MAlonzo.Code.Data.List.Membership.Setoid.du_mapWith'8712'_64
      (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v0)
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 AgdaAny
v2 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v1)))