{-# 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.String 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.Char
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Char.Properties
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.Extrema
import qualified MAlonzo.Code.Data.List.Membership.DecSetoid
import qualified MAlonzo.Code.Data.List.Membership.Propositional
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.Any
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Data.Sum.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.String._.argmax
d_argmax_6 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> Integer) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmax_6 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmax_6 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.String._.argmax-all
d_argmax'45'all_8 ::
  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_8 :: 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_8 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.String._.argmax-sel
d_argmax'45'sel_10 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmax'45'sel_10 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmax'45'sel_10 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.String._.argmax[xs]<argmax[ys]⁺
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_12 ::
  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'_12 :: 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'_12 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.String._.argmax[xs]≤argmax[ys]⁺
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_14 ::
  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'_14 :: 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'_14 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.String._.argmin
d_argmin_16 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> Integer) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmin_16 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmin_16 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.String._.argmin-all
d_argmin'45'all_18 ::
  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_18 :: 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_18 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.String._.argmin-sel
d_argmin'45'sel_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Integer) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmin'45'sel_20 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmin'45'sel_20 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.String._.argmin[xs]<argmin[ys]⁺
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_22 ::
  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'_22 :: 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'_22 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.String._.argmin[xs]≤argmin[ys]⁺
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_24 ::
  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'_24 :: 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'_24 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.String._.f[argmax]<v⁺
d_f'91'argmax'93''60'v'8314'_26 ::
  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'_26 :: 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'_26 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.String._.f[argmax]≈f[v]⁺
d_f'91'argmax'93''8776'f'91'v'93''8314'_28 ::
  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'_28 :: 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'_28 = 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.String._.f[argmax]≤v⁺
d_f'91'argmax'93''8804'v'8314'_30 ::
  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'_30 :: 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'_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]
 -> 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.String._.f[argmin]<v⁺
d_f'91'argmin'93''60'v'8314'_32 ::
  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'_32 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_f'91'argmin'93''60'v'8314'_32 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.String._.f[argmin]≈f[v]⁺
d_f'91'argmin'93''8776'f'91'v'93''8314'_34 ::
  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'_34 :: 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'_34 = 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.String._.f[argmin]≤f[xs]
d_f'91'argmin'93''8804'f'91'xs'93'_36 ::
  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'_36 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'argmin'93''8804'f'91'xs'93'_36 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.String._.f[argmin]≤f[⊤]
d_f'91'argmin'93''8804'f'91''8868''93'_38 ::
  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'_38 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
d_f'91'argmin'93''8804'f'91''8868''93'_38 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.String._.f[argmin]≤v⁺
d_f'91'argmin'93''8804'v'8314'_40 ::
  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'_40 :: 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'_40 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.String._.f[xs]≤f[argmax]
d_f'91'xs'93''8804'f'91'argmax'93'_42 ::
  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'_42 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'xs'93''8804'f'91'argmax'93'_42 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.String._.f[⊥]≤f[argmax]
d_f'91''8869''93''8804'f'91'argmax'93'_44 ::
  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'_44 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> AgdaAny
-> [AgdaAny]
-> T__'8804'__22
d_f'91''8869''93''8804'f'91'argmax'93'_44 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.String._.max
d_max_46 :: Integer -> [Integer] -> Integer
d_max_46 :: Integer -> [Integer] -> Integer
d_max_46
  = (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.String._.max-mono-⊆
d_max'45'mono'45''8838'_48 ::
  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'_48 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8804'__22
-> (Integer -> T_Any_34 -> T_Any_34)
-> T__'8804'__22
d_max'45'mono'45''8838'_48
  = (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.String._.max<v⁺
d_max'60'v'8314'_50 ::
  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'_50 :: Integer -> Integer -> [Integer] -> T_Σ_14 -> T_All_44 -> T_Σ_14
d_max'60'v'8314'_50 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.String._.max[xs]<max[ys]⁺
d_max'91'xs'93''60'max'91'ys'93''8314'_52 ::
  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'_52 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_max'91'xs'93''60'max'91'ys'93''8314'_52
  = (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.String._.max[xs]≤max[ys]⁺
d_max'91'xs'93''8804'max'91'ys'93''8314'_54 ::
  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'_54 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
d_max'91'xs'93''8804'max'91'ys'93''8314'_54
  = (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.String._.max≈v⁺
d_max'8776'v'8314'_56 ::
  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'_56 :: Integer
-> Integer
-> [Integer]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
d_max'8776'v'8314'_56 = Integer
-> Integer
-> [Integer]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.String._.max≤v⁺
d_max'8804'v'8314'_58 ::
  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'_58 :: Integer
-> Integer
-> [Integer]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
d_max'8804'v'8314'_58 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.String._.min
d_min_60 :: Integer -> [Integer] -> Integer
d_min_60 :: Integer -> [Integer] -> Integer
d_min_60
  = (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.String._.min-mono-⊆
d_min'45'mono'45''8838'_62 ::
  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'_62 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8804'__22
-> (Integer -> T_Any_34 -> T_Any_34)
-> T__'8804'__22
d_min'45'mono'45''8838'_62
  = (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.String._.min<v⁺
d_min'60'v'8314'_64 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_min'60'v'8314'_64 :: Integer -> Integer -> [Integer] -> T__'8846'__30 -> T_Σ_14
d_min'60'v'8314'_64
  = (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.String._.min[xs]<min[ys]⁺
d_min'91'xs'93''60'min'91'ys'93''8314'_66 ::
  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'_66 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_min'91'xs'93''60'min'91'ys'93''8314'_66
  = (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.String._.min[xs]≤min[ys]⁺
d_min'91'xs'93''8804'min'91'ys'93''8314'_68 ::
  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'_68 :: Integer
-> Integer
-> [Integer]
-> [Integer]
-> T__'8846'__30
-> T_All_44
-> T__'8804'__22
d_min'91'xs'93''8804'min'91'ys'93''8314'_68
  = (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.String._.min≈v⁺
d_min'8776'v'8314'_70 ::
  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'_70 :: Integer
-> Integer
-> [Integer]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
d_min'8776'v'8314'_70 = Integer
-> Integer
-> [Integer]
-> T_Any_34
-> T_All_44
-> T__'8804'__22
-> T__'8801'__12
forall a. a
erased
-- Data.String._.min≤v⁺
d_min'8804'v'8314'_72 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_min'8804'v'8314'_72 :: Integer -> Integer -> [Integer] -> T__'8846'__30 -> T__'8804'__22
d_min'8804'v'8314'_72
  = (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.String._.min≤xs
d_min'8804'xs_74 ::
  Integer ->
  [Integer] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_min'8804'xs_74 :: Integer -> [Integer] -> T_All_44
d_min'8804'xs_74
  = (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.String._.min≤⊤
d_min'8804''8868'_76 ::
  Integer -> [Integer] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_min'8804''8868'_76 :: Integer -> [Integer] -> T__'8804'__22
d_min'8804''8868'_76
  = (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.String._.v<f[argmax]⁺
d_v'60'f'91'argmax'93''8314'_78 ::
  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'_78 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Integer)
-> Integer
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_v'60'f'91'argmax'93''8314'_78 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.String._.v<f[argmin]⁺
d_v'60'f'91'argmin'93''8314'_80 ::
  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'_80 :: 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'_80 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.String._.v<max⁺
d_v'60'max'8314'_82 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'max'8314'_82 :: Integer -> Integer -> [Integer] -> T__'8846'__30 -> T_Σ_14
d_v'60'max'8314'_82
  = (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.String._.v<min⁺
d_v'60'min'8314'_84 ::
  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'_84 :: Integer -> Integer -> [Integer] -> T_Σ_14 -> T_All_44 -> T_Σ_14
d_v'60'min'8314'_84 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.String._.v≤f[argmax]⁺
d_v'8804'f'91'argmax'93''8314'_86 ::
  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'_86 :: 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'_86 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.String._.v≤f[argmin]⁺
d_v'8804'f'91'argmin'93''8314'_88 ::
  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'_88 :: 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'_88 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.String._.v≤max⁺
d_v'8804'max'8314'_90 ::
  Integer ->
  Integer ->
  [Integer] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_v'8804'max'8314'_90 :: Integer -> Integer -> [Integer] -> T__'8846'__30 -> T__'8804'__22
d_v'8804'max'8314'_90
  = (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.String._.v≤min⁺
d_v'8804'min'8314'_92 ::
  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'_92 :: Integer
-> Integer
-> [Integer]
-> T__'8804'__22
-> T_All_44
-> T__'8804'__22
d_v'8804'min'8314'_92 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.String._.xs≤max
d_xs'8804'max_94 ::
  Integer ->
  [Integer] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_xs'8804'max_94 :: Integer -> [Integer] -> T_All_44
d_xs'8804'max_94
  = (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.String._.⊥≤max
d_'8869''8804'max_96 ::
  Integer -> [Integer] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
d_'8869''8804'max_96 :: Integer -> [Integer] -> T__'8804'__22
d_'8869''8804'max_96
  = (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.String._._∈_
d__'8712'__100 ::
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] -> ()
d__'8712'__100 :: T_Char_6 -> [T_Char_6] -> T_Level_18
d__'8712'__100 = T_Char_6 -> [T_Char_6] -> T_Level_18
forall a. a
erased
-- Data.String._._∈?_
d__'8712''63'__102 ::
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8712''63'__102 :: T_Char_6 -> [T_Char_6] -> T_Dec_20
d__'8712''63'__102
  = let v0 :: T_Char_6 -> T_Char_6 -> T_Dec_20
v0 = T_Char_6 -> T_Char_6 -> T_Dec_20
MAlonzo.Code.Data.Char.Properties.d__'8799'__14 in
    AgdaAny -> T_Char_6 -> [T_Char_6] -> T_Dec_20
forall a b. a -> b
coe
      ((T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Membership.DecSetoid.du__'8712''63'__60
         (((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_90)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_90
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
            ((T_Char_6 -> T_Char_6 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
v0)))
-- Data.String._._∉_
d__'8713'__104 ::
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] -> ()
d__'8713'__104 :: T_Char_6 -> [T_Char_6] -> T_Level_18
d__'8713'__104 = T_Char_6 -> [T_Char_6] -> T_Level_18
forall a. a
erased
-- Data.String._._∉?_
d__'8713''63'__106 ::
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8713''63'__106 :: T_Char_6 -> [T_Char_6] -> T_Dec_20
d__'8713''63'__106
  = let v0 :: T_Char_6 -> T_Char_6 -> T_Dec_20
v0 = T_Char_6 -> T_Char_6 -> T_Dec_20
MAlonzo.Code.Data.Char.Properties.d__'8799'__14 in
    AgdaAny -> T_Char_6 -> [T_Char_6] -> T_Dec_20
forall a b. a -> b
coe
      ((T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Membership.DecSetoid.du__'8713''63'__68
         (((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_90)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_90
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
            ((T_Char_6 -> T_Char_6 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
v0)))
-- Data.String._._∷=_
d__'8759''61'__108 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  (MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> ()) ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6]
d__'8759''61'__108 :: T_Level_18
-> [T_Char_6]
-> (T_Char_6 -> T_Level_18)
-> T_Any_34
-> T_Char_6
-> [T_Char_6]
d__'8759''61'__108
  = (T_Level_18
 -> [AgdaAny]
 -> (AgdaAny -> T_Level_18)
 -> T_Any_34
 -> AgdaAny
 -> [AgdaAny])
-> T_Level_18
-> [T_Char_6]
-> (T_Char_6 -> T_Level_18)
-> T_Any_34
-> T_Char_6
-> [T_Char_6]
forall a b. a -> b
coe T_Level_18
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> T_Any_34
-> AgdaAny
-> [AgdaAny]
MAlonzo.Code.Data.List.Membership.Setoid.du__'8759''61'__52
-- Data.String._._≢∈_
d__'8802''8712'__110 ::
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> ()
d__'8802''8712'__110 :: T_Char_6
-> T_Char_6 -> [T_Char_6] -> T_Any_34 -> T_Any_34 -> T_Level_18
d__'8802''8712'__110 = T_Char_6
-> T_Char_6 -> [T_Char_6] -> T_Any_34 -> T_Any_34 -> T_Level_18
forall a. a
erased
-- Data.String._._─_
d__'9472'__112 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> ()) ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6]
d__'9472'__112 :: T_Level_18
-> (T_Char_6 -> T_Level_18) -> [T_Char_6] -> T_Any_34 -> [T_Char_6]
d__'9472'__112
  = (T_Level_18
 -> (AgdaAny -> T_Level_18) -> [AgdaAny] -> T_Any_34 -> [AgdaAny])
-> T_Level_18
-> (T_Char_6 -> T_Level_18)
-> [T_Char_6]
-> T_Any_34
-> [T_Char_6]
forall a b. a -> b
coe T_Level_18
-> (AgdaAny -> T_Level_18) -> [AgdaAny] -> T_Any_34 -> [AgdaAny]
MAlonzo.Code.Data.List.Membership.Setoid.du__'9472'__54
-- Data.String._.find
d_find_114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> ()) ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_find_114 :: T_Level_18
-> (T_Char_6 -> T_Level_18) -> [T_Char_6] -> T_Any_34 -> T_Σ_14
d_find_114 T_Level_18
v0 T_Char_6 -> T_Level_18
v1 [T_Char_6]
v2 T_Any_34
v3
  = (T_Setoid_46 -> [AgdaAny] -> T_Any_34 -> T_Σ_14)
-> AgdaAny -> [T_Char_6] -> T_Any_34 -> T_Σ_14
forall a b. a -> b
coe
      T_Setoid_46 -> [AgdaAny] -> T_Any_34 -> T_Σ_14
MAlonzo.Code.Data.List.Membership.Setoid.du_find_86
      (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
      [T_Char_6]
v2 T_Any_34
v3
-- Data.String._.lose
d_lose_116 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> ()) ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny -> MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
d_lose_116 :: T_Level_18
-> (T_Char_6 -> T_Level_18)
-> T_Char_6
-> [T_Char_6]
-> T_Any_34
-> AgdaAny
-> T_Any_34
d_lose_116 T_Level_18
v0 T_Char_6 -> T_Level_18
v1 T_Char_6
v2 [T_Char_6]
v3
  = (AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> T_Char_6 -> [T_Char_6] -> T_Any_34 -> AgdaAny -> T_Any_34
forall a b. a -> b
coe
      AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Membership.Propositional.du_lose_50 T_Char_6
v2 [T_Char_6]
v3
-- Data.String._.mapWith∈
d_mapWith'8712'_118 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  (MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 -> AgdaAny) ->
  [AgdaAny]
d_mapWith'8712'_118 :: T_Level_18
-> T_Level_18
-> [T_Char_6]
-> (T_Char_6 -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
d_mapWith'8712'_118 T_Level_18
v0 T_Level_18
v1 [T_Char_6]
v2 T_Char_6 -> T_Any_34 -> AgdaAny
v3
  = (T_Setoid_46
 -> [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> [AgdaAny])
-> AgdaAny
-> [T_Char_6]
-> (T_Char_6 -> T_Any_34 -> AgdaAny)
-> [AgdaAny]
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_Char_6]
v2 T_Char_6 -> T_Any_34 -> AgdaAny
v3
-- Data.String.toVec
d_toVec_122 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_toVec_122 :: T_String_6 -> T_Vec_28
d_toVec_122 T_String_6
v0
  = ([AgdaAny] -> T_Vec_28) -> AgdaAny -> T_Vec_28
forall a b. a -> b
coe
      [AgdaAny] -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_fromList_600
      ((T_String_6 -> [T_Char_6]) -> T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6 -> [T_Char_6]
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0)
-- Data.String.fromVec
d_fromVec_128 ::
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_fromVec_128 :: Integer -> T_Vec_28 -> T_String_6
d_fromVec_128 ~Integer
v0 T_Vec_28
v1 = T_Vec_28 -> T_String_6
du_fromVec_128 T_Vec_28
v1
du_fromVec_128 ::
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_fromVec_128 :: T_Vec_28 -> T_String_6
du_fromVec_128 T_Vec_28
v0
  = ([T_Char_6] -> T_String_6) -> AgdaAny -> T_String_6
forall a b. a -> b
coe
      [T_Char_6] -> T_String_6
MAlonzo.Code.Agda.Builtin.String.d_primStringFromList_14
      ((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_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v0))
-- Data.String.parensIfSpace
d_parensIfSpace_130 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_parensIfSpace_130 :: T_String_6 -> T_String_6
d_parensIfSpace_130 T_String_6
v0
  = (Bool -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_String_6
forall a b. a -> b
coe
      Bool -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Bool.Base.du_if_then_else__44
      ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
         ((T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_DecSetoid_90 -> AgdaAny -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Membership.DecSetoid.du__'8712''63'__60
            (((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_90)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecSetoid_90
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
               ((T_Char_6 -> T_Char_6 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
MAlonzo.Code.Data.Char.Properties.d__'8799'__14))
            (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
' ')
            ((T_String_6 -> [T_Char_6]) -> T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6 -> [T_Char_6]
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0)))
      ((T_String_6 -> T_String_6) -> T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6 -> T_String_6
MAlonzo.Code.Data.String.Base.d_parens_46 T_String_6
v0) (T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6
v0)
-- Data.String.rectangle
d_rectangle_136 ::
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_rectangle_136 :: Integer -> T_Vec_28 -> T_Vec_28 -> T_Vec_28
d_rectangle_136 ~Integer
v0 T_Vec_28
v1 T_Vec_28
v2 = T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136 T_Vec_28
v1 T_Vec_28
v2
du_rectangle_136 ::
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
du_rectangle_136 :: T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136 T_Vec_28
v0 T_Vec_28
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Vec_28 -> T_Vec_28 -> T_Vec_28)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Vec_28
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> T_Vec_28 -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_zipWith_242
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 ((T_Vec_28 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Vec_28 -> Integer
du_width_148 (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v1)))) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v0)
      (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v1)
-- Data.String._.sizes
d_sizes_146 ::
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> [Integer]
d_sizes_146 :: Integer -> T_Vec_28 -> T_Vec_28 -> [Integer]
d_sizes_146 ~Integer
v0 ~T_Vec_28
v1 T_Vec_28
v2 = T_Vec_28 -> [Integer]
du_sizes_146 T_Vec_28
v2
du_sizes_146 :: MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> [Integer]
du_sizes_146 :: T_Vec_28 -> [Integer]
du_sizes_146 T_Vec_28
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
      ((T_String_6 -> Integer) -> AgdaAny
forall a b. a -> b
coe T_String_6 -> Integer
MAlonzo.Code.Data.String.Base.d_length_22)
      ((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_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v0))
-- Data.String._.width
d_width_148 ::
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_width_148 :: Integer -> T_Vec_28 -> T_Vec_28 -> Integer
d_width_148 ~Integer
v0 ~T_Vec_28
v1 T_Vec_28
v2 = T_Vec_28 -> Integer
du_width_148 T_Vec_28
v2
du_width_148 :: MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
du_width_148 :: T_Vec_28 -> Integer
du_width_148 T_Vec_28
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_Vec_28 -> [Integer]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Vec_28 -> [Integer]
du_sizes_146 (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v0))
-- Data.String.rectangleˡ
d_rectangle'737'_156 ::
  Integer ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_rectangle'737'_156 :: Integer -> T_Char_6 -> T_Vec_28 -> T_Vec_28
d_rectangle'737'_156 Integer
v0 T_Char_6
v1
  = (T_Vec_28 -> T_Vec_28 -> T_Vec_28)
-> AgdaAny -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe
      T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136
      ((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)
         ((T_Char_6 -> Integer -> T_String_6 -> T_String_6)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Char_6 -> Integer -> T_String_6 -> T_String_6
MAlonzo.Code.Data.String.Base.d_padLeft_60 (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
v1)))
-- Data.String.rectangleʳ
d_rectangle'691'_162 ::
  Integer ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_rectangle'691'_162 :: Integer -> T_Char_6 -> T_Vec_28 -> T_Vec_28
d_rectangle'691'_162 Integer
v0 T_Char_6
v1
  = (T_Vec_28 -> T_Vec_28 -> T_Vec_28)
-> AgdaAny -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe
      T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136
      ((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)
         ((T_Char_6 -> Integer -> T_String_6 -> T_String_6)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Char_6 -> Integer -> T_String_6 -> T_String_6
MAlonzo.Code.Data.String.Base.d_padRight_70 (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
v1)))
-- Data.String.rectangleᶜ
d_rectangle'7580'_168 ::
  Integer ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_rectangle'7580'_168 :: Integer -> T_Char_6 -> T_Char_6 -> T_Vec_28 -> T_Vec_28
d_rectangle'7580'_168 Integer
v0 T_Char_6
v1 T_Char_6
v2
  = (T_Vec_28 -> T_Vec_28 -> T_Vec_28)
-> AgdaAny -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe
      T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136
      ((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)
         ((T_Char_6 -> T_Char_6 -> Integer -> T_String_6 -> T_String_6)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> Integer -> T_String_6 -> T_String_6
MAlonzo.Code.Data.String.Base.d_padBoth_80 (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
v1) (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
v2)))