| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Extrema
Documentation
d__'60'__80 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → () Source #
d_argmin_118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_argmin_118 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_argmax_122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_argmax_122 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_min_126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → [AgdaAny] → AgdaAny Source #
du_min_126 ∷ T_TotalOrder_652 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_max_128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → [AgdaAny] → AgdaAny Source #
du_max_128 ∷ T_TotalOrder_652 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_f'91'argmin'93''8804'v'8314'_146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_f'91'argmin'93''8804'v'8314'_146 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_f'91'argmin'93''60'v'8314'_156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_f'91'argmin'93''60'v'8314'_156 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_v'8804'f'91'argmin'93''8314'_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_v'8804'f'91'argmin'93''8314'_166 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_v'60'f'91'argmin'93''8314'_176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_v'60'f'91'argmin'93''8314'_176 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_f'91'argmin'93''8804'f'91''8868''93'_182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_f'91'argmin'93''8804'f'91''8868''93'_182 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_f'91'argmin'93''8804'f'91'xs'93'_194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
du_f'91'argmin'93''8804'f'91'xs'93'_194 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
d_f'91'argmin'93''8776'f'91'v'93''8314'_208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
du_f'91'argmin'93''8776'f'91'v'93''8314'_208 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_234 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_262 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_argmin'45'sel_278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
du_argmin'45'sel_278 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
d_argmin'45'all_290 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → (AgdaAny → ()) → AgdaAny → T_All_44 → AgdaAny Source #
du_argmin'45'all_290 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_v'8804'f'91'argmax'93''8314'_352 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_v'8804'f'91'argmax'93''8314'_352 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_v'60'f'91'argmax'93''8314'_362 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_v'60'f'91'argmax'93''8314'_362 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_f'91'argmax'93''8804'v'8314'_372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_f'91'argmax'93''8804'v'8314'_372 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_f'91'argmax'93''60'v'8314'_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_f'91'argmax'93''60'v'8314'_382 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_f'91''8869''93''8804'f'91'argmax'93'_388 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_f'91''8869''93''8804'f'91'argmax'93'_388 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_f'91'xs'93''8804'f'91'argmax'93'_400 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
du_f'91'xs'93''8804'f'91'argmax'93'_400 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
d_f'91'argmax'93''8776'f'91'v'93''8314'_414 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
du_f'91'argmax'93''8776'f'91'v'93''8314'_414 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_440 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_468 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_argmax'45'sel_484 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
du_argmax'45'sel_484 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
d_argmax'45'all_496 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_argmax'45'all_496 ∷ T_TotalOrder_652 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_min'8804'v'8314'_550 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_min'8804'v'8314'_550 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_min'60'v'8314'_560 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_min'60'v'8314'_560 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_v'8804'min'8314'_570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_v'8804'min'8314'_570 ∷ T_TotalOrder_652 → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_v'60'min'8314'_580 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_v'60'min'8314'_580 ∷ T_TotalOrder_652 → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_min'8804''8868'_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_min'8804'xs_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → [AgdaAny] → T_All_44 Source #
du_min'8804'xs_594 ∷ T_TotalOrder_652 → AgdaAny → [AgdaAny] → T_All_44 Source #
d_min'8776'v'8314'_604 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
du_min'8776'v'8314'_604 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
d_min'91'xs'93''8804'min'91'ys'93''8314'_620 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
du_min'91'xs'93''8804'min'91'ys'93''8314'_620 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
d_min'91'xs'93''60'min'91'ys'93''8314'_636 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
du_min'91'xs'93''60'min'91'ys'93''8314'_636 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_min'45'mono'45''8838'_646 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
du_min'45'mono'45''8838'_646 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
d_'46'extendedlambda0_652 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → T_Any_34 → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_max'8804'v'8314'_662 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_max'8804'v'8314'_662 ∷ T_TotalOrder_652 → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_max'60'v'8314'_672 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_max'60'v'8314'_672 ∷ T_TotalOrder_652 → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_v'8804'max'8314'_682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_v'8804'max'8314'_682 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_v'60'max'8314'_692 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_v'60'max'8314'_692 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_'8869''8804'max_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_xs'8804'max_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → [AgdaAny] → T_All_44 Source #
du_xs'8804'max_706 ∷ T_TotalOrder_652 → AgdaAny → [AgdaAny] → T_All_44 Source #
d_max'8776'v'8314'_716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
du_max'8776'v'8314'_716 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
d_max'91'xs'93''8804'max'91'ys'93''8314'_732 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
du_max'91'xs'93''8804'max'91'ys'93''8314'_732 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
d_max'91'xs'93''60'max'91'ys'93''8314'_748 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
du_max'91'xs'93''60'max'91'ys'93''8314'_748 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_max'45'mono'45''8838'_758 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
du_max'45'mono'45''8838'_758 ∷ T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
d_'46'extendedlambda1_764 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → T_Any_34 → AgdaAny → T__'8801'__12 → AgdaAny Source #