Documentation

d_argmax_6 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → AgdaAny Source #

d_argmax'45'all_8 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → Integer) → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #

d_argmax'45'sel_10 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #

d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_12 ∷ T_Level_18 → () → (AgdaAny → Integer) → (AgdaAny → Integer) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #

d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_14 ∷ T_Level_18 → () → (AgdaAny → Integer) → (AgdaAny → Integer) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T__'8804'__22 Source #

d_argmin_16 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → AgdaAny Source #

d_argmin'45'all_18 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → (AgdaAny → ()) → AgdaAny → T_All_44 → AgdaAny Source #

d_argmin'45'sel_20 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #

d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_22 ∷ T_Level_18 → () → (AgdaAny → Integer) → (AgdaAny → Integer) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #

d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_24 ∷ T_Level_18 → () → (AgdaAny → Integer) → (AgdaAny → Integer) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T__'8804'__22 Source #

d_f'91'argmax'93''60'v'8314'_26 ∷ T_Level_18 → () → (AgdaAny → Integer) → Integer → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #

d_f'91'argmax'93''8776'f'91'v'93''8314'_28 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → T__'8804'__22 → T__'8801'__12 Source #

d_f'91'argmax'93''8804'v'8314'_30 ∷ T_Level_18 → () → (AgdaAny → Integer) → Integer → AgdaAny → [AgdaAny] → T__'8804'__22 → T_All_44 → T__'8804'__22 Source #

d_f'91'argmin'93''60'v'8314'_32 ∷ T_Level_18 → () → (AgdaAny → Integer) → Integer → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #

d_f'91'argmin'93''8776'f'91'v'93''8314'_34 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → T__'8804'__22 → T__'8801'__12 Source #

d_f'91'argmin'93''8804'f'91'xs'93'_36 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → T_All_44 Source #

d_f'91'argmin'93''8804'f'91''8868''93'_38 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → T__'8804'__22 Source #

d_f'91'argmin'93''8804'v'8314'_40 ∷ T_Level_18 → () → (AgdaAny → Integer) → Integer → AgdaAny → [AgdaAny] → T__'8846'__30 → T__'8804'__22 Source #

d_f'91'xs'93''8804'f'91'argmax'93'_42 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → T_All_44 Source #

d_f'91''8869''93''8804'f'91'argmax'93'_44 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → T__'8804'__22 Source #

d_max_46 ∷ Integer → [Integer] → Integer Source #

d_max'45'mono'45''8838'_48 ∷ Integer → Integer → [Integer] → [Integer] → T__'8804'__22 → (Integer → T_Any_34 → T_Any_34) → T__'8804'__22 Source #

d_max'60'v'8314'_50 ∷ Integer → Integer → [Integer] → T_Σ_14 → T_All_44 → T_Σ_14 Source #

d_max'91'xs'93''60'max'91'ys'93''8314'_52 ∷ Integer → Integer → [Integer] → [Integer] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #

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 Source #

d_max'8776'v'8314'_56 ∷ Integer → Integer → [Integer] → T_Any_34 → T_All_44 → T__'8804'__22 → T__'8801'__12 Source #

d_max'8804'v'8314'_58 ∷ Integer → Integer → [Integer] → T__'8804'__22 → T_All_44 → T__'8804'__22 Source #

d_min_60 ∷ Integer → [Integer] → Integer Source #

d_min'45'mono'45''8838'_62 ∷ Integer → Integer → [Integer] → [Integer] → T__'8804'__22 → (Integer → T_Any_34 → T_Any_34) → T__'8804'__22 Source #

d_min'60'v'8314'_64 ∷ Integer → Integer → [Integer] → T__'8846'__30 → T_Σ_14 Source #

d_min'91'xs'93''60'min'91'ys'93''8314'_66 ∷ Integer → Integer → [Integer] → [Integer] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #

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 Source #

d_min'8776'v'8314'_70 ∷ Integer → Integer → [Integer] → T_Any_34 → T_All_44 → T__'8804'__22 → T__'8801'__12 Source #

d_min'8804'v'8314'_72 ∷ Integer → Integer → [Integer] → T__'8846'__30 → T__'8804'__22 Source #

d_min'8804'xs_74 ∷ Integer → [Integer] → T_All_44 Source #

d_min'8804''8868'_76 ∷ Integer → [Integer] → T__'8804'__22 Source #

d_v'60'f'91'argmax'93''8314'_78 ∷ T_Level_18 → () → (AgdaAny → Integer) → Integer → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #

d_v'60'f'91'argmin'93''8314'_80 ∷ T_Level_18 → () → (AgdaAny → Integer) → Integer → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #

d_v'60'max'8314'_82 ∷ Integer → Integer → [Integer] → T__'8846'__30 → T_Σ_14 Source #

d_v'60'min'8314'_84 ∷ Integer → Integer → [Integer] → T_Σ_14 → T_All_44 → T_Σ_14 Source #

d_v'8804'f'91'argmax'93''8314'_86 ∷ T_Level_18 → () → (AgdaAny → Integer) → Integer → AgdaAny → [AgdaAny] → T__'8846'__30 → T__'8804'__22 Source #

d_v'8804'f'91'argmin'93''8314'_88 ∷ T_Level_18 → () → (AgdaAny → Integer) → Integer → AgdaAny → [AgdaAny] → T__'8804'__22 → T_All_44 → T__'8804'__22 Source #

d_v'8804'max'8314'_90 ∷ Integer → Integer → [Integer] → T__'8846'__30 → T__'8804'__22 Source #

d_v'8804'min'8314'_92 ∷ Integer → Integer → [Integer] → T__'8804'__22 → T_All_44 → T__'8804'__22 Source #

d_xs'8804'max_94 ∷ Integer → [Integer] → T_All_44 Source #

d_'8869''8804'max_96 ∷ Integer → [Integer] → T__'8804'__22 Source #

d__'8712'__100 ∷ T_Char_6 → [T_Char_6] → () Source #

d__'8712''63'__102 ∷ T_Char_6 → [T_Char_6] → T_Dec_20 Source #

d__'8713'__104 ∷ T_Char_6 → [T_Char_6] → () Source #

d__'8713''63'__106 ∷ T_Char_6 → [T_Char_6] → T_Dec_20 Source #

d__'8759''61'__108 ∷ T_Level_18 → [T_Char_6] → (T_Char_6 → ()) → T_Any_34 → T_Char_6 → [T_Char_6] Source #

d__'8802''8712'__110 ∷ T_Char_6 → T_Char_6 → [T_Char_6] → T_Any_34 → T_Any_34 → () Source #

d__'9472'__112 ∷ T_Level_18 → (T_Char_6 → ()) → [T_Char_6] → T_Any_34 → [T_Char_6] Source #

d_find_114 ∷ T_Level_18 → (T_Char_6 → ()) → [T_Char_6] → T_Any_34 → T_Σ_14 Source #

d_lose_116 ∷ T_Level_18 → (T_Char_6 → ()) → T_Char_6 → [T_Char_6] → T_Any_34 → AgdaAny → T_Any_34 Source #

d_mapWith'8712'_118 ∷ T_Level_18 → () → [T_Char_6] → (T_Char_6 → T_Any_34 → AgdaAny) → [AgdaAny] Source #

d_toVec_122 ∷ T_String_6 → T_Vec_28 Source #

d_fromVec_128 ∷ Integer → T_Vec_28 → T_String_6 Source #

du_fromVec_128 ∷ T_Vec_28 → T_String_6 Source #

d_parensIfSpace_130 ∷ T_String_6 → T_String_6 Source #

d_rectangle_136 ∷ Integer → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du_rectangle_136 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_sizes_146 ∷ Integer → T_Vec_28 → T_Vec_28 → [Integer] Source #

du_sizes_146 ∷ T_Vec_28 → [Integer] Source #

d_width_148 ∷ Integer → T_Vec_28 → T_Vec_28 → Integer Source #

du_width_148 ∷ T_Vec_28 → Integer Source #

d_rectangle'737'_156 ∷ Integer → T_Char_6 → T_Vec_28 → T_Vec_28 Source #

d_rectangle'691'_162 ∷ Integer → T_Char_6 → T_Vec_28 → T_Vec_28 Source #

d_rectangle'7580'_168 ∷ Integer → T_Char_6 → T_Char_6 → T_Vec_28 → T_Vec_28 Source #