Documentation

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

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

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

d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_16 ∷ 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'_18 ∷ T_Level_18 → () → (AgdaAny → Integer) → (AgdaAny → Integer) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T__'8804'__22 Source #

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

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

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

d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_26 ∷ 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'_28 ∷ 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'_30 ∷ 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'_32 ∷ 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'_34 ∷ 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'_36 ∷ 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'_38 ∷ 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'_40 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → T_All_44 Source #

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

d_f'91'argmin'93''8804'v'8314'_44 ∷ 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'_46 ∷ T_Level_18 → () → (AgdaAny → Integer) → AgdaAny → [AgdaAny] → T_All_44 Source #

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

d_max_50 ∷ Integer → [Integer] → Integer Source #

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

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

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

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

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

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

d_min_64 ∷ Integer → [Integer] → Integer Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_Vec'8804'_126 ∷ p → p → p → () Source #

data T_Vec'8804'_126 Source #

d_length_138 ∷ T_Vec'8804'_126 → Integer Source #

d_vec_140 ∷ T_Vec'8804'_126 → T_Vec_28 Source #

d_isBounded_148 ∷ T_Level_18 → () → Integer → T_Vec'8804'_126 → T__'8804'__22 Source #

du_isBounded_148 ∷ Integer → T_Vec'8804'_126 → T__'8804'__22 Source #

d_toVec_156 ∷ T_Vec'8804'_126 → T_Vec_28 Source #

d_fromVec_162 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Vec'8804'_126 Source #

du_fromVec_162 ∷ Integer → T_Vec_28 → T_Vec'8804'_126 Source #

d_padRight_166 ∷ T_Level_18 → () → Integer → AgdaAny → T_Vec'8804'_126 → T_Vec_28 Source #

du_padRight_166 ∷ Integer → AgdaAny → T_Vec'8804'_126 → T_Vec_28 Source #

d_padLeft_182 ∷ T_Level_18 → () → Integer → AgdaAny → T_Vec'8804'_126 → T_Vec_28 Source #

du_padLeft_182 ∷ Integer → AgdaAny → T_Vec'8804'_126 → T_Vec_28 Source #

d_split_206 ∷ Integer → Integer → T__'8801'__12 Source #

d_padBoth_220 ∷ T_Level_18 → () → Integer → AgdaAny → AgdaAny → T_Vec'8804'_126 → T_Vec_28 Source #

du_padBoth_220 ∷ Integer → AgdaAny → AgdaAny → T_Vec'8804'_126 → T_Vec_28 Source #

d_fromList_244 ∷ T_Level_18 → () → [AgdaAny] → T_Vec'8804'_126 Source #

du_fromList_244 ∷ [AgdaAny] → T_Vec'8804'_126 Source #

d_toList_246 ∷ T_Level_18 → () → Integer → T_Vec'8804'_126 → [AgdaAny] Source #

du_toList_246 ∷ T_Vec'8804'_126 → [AgdaAny] Source #

d_replicate_250 ∷ Integer → Integer → T_Level_18 → () → T__'8804'__22 → AgdaAny → T_Vec'8804'_126 Source #

du_replicate_250 ∷ Integer → AgdaAny → T_Vec'8804'_126 Source #

d_'91''93'_256 ∷ T_Level_18 → () → Integer → T_Vec'8804'_126 Source #

du_'91''93'_256 ∷ T_Vec'8804'_126 Source #

d__'8759'__258 ∷ T_Level_18 → () → Integer → AgdaAny → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

du__'8759'__258 ∷ AgdaAny → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

d_'8804''45'cast_268 ∷ Integer → Integer → T_Level_18 → () → T__'8804'__22 → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

du_'8804''45'cast_268 ∷ T_Vec'8804'_126 → T_Vec'8804'_126 Source #

d_'8801''45'cast_278 ∷ Integer → Integer → T_Level_18 → () → T__'8801'__12 → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

du_'8801''45'cast_278 ∷ T_Vec'8804'_126 → T_Vec'8804'_126 Source #

d_map_282 ∷ T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → AgdaAny) → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

du_map_282 ∷ (AgdaAny → AgdaAny) → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

d_reverse_290 ∷ T_Level_18 → () → Integer → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

du_reverse_290 ∷ T_Vec'8804'_126 → T_Vec'8804'_126 Source #

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

du_alignWith_296 ∷ (T_These_38 → AgdaAny) → T_Vec'8804'_126 → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

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

du_zipWith_308 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec'8804'_126 → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

d_zip_320 ∷ T_Level_18 → () → Integer → T_Level_18 → () → T_Vec'8804'_126 → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

du_zip_320 ∷ T_Vec'8804'_126 → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

d_align_322 ∷ T_Level_18 → () → Integer → T_Level_18 → () → T_Vec'8804'_126 → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

du_align_322 ∷ T_Vec'8804'_126 → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

d_take_326 ∷ T_Level_18 → () → Integer → Integer → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

du_take_326 ∷ Integer → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

d_drop_344 ∷ T_Level_18 → () → Integer → Integer → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

du_drop_344 ∷ Integer → T_Vec'8804'_126 → T_Vec'8804'_126 Source #

d_rectangle_362 ∷ T_Level_18 → () → [T_Σ_14] → T_Σ_14 Source #

du_rectangle_362 ∷ [T_Σ_14] → T_Σ_14 Source #

d_sizes_372 ∷ T_Level_18 → () → [T_Σ_14] → [Integer] Source #

du_sizes_372 ∷ [T_Σ_14] → [Integer] Source #

d_width_374 ∷ T_Level_18 → () → [T_Σ_14] → Integer Source #

du_width_374 ∷ [T_Σ_14] → Integer Source #

d_all'8804'_378 ∷ T_Level_18 → () → [T_Σ_14] → T_All_44 Source #

du_all'8804'_378 ∷ [T_Σ_14] → T_All_44 Source #

d_padded_380 ∷ T_Level_18 → () → [T_Σ_14] → [T_Vec'8804'_126] Source #

du_padded_380 ∷ [T_Σ_14] → [T_Vec'8804'_126] Source #