| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Extrema
Documentation
d__'60'__102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → () Source #
d_argmin_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_argmin_140 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_argmax_144 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_argmax_144 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_min_148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → [AgdaAny] → AgdaAny Source #
du_min_148 ∷ T_TotalOrder_986 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_max_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → [AgdaAny] → AgdaAny Source #
du_max_150 ∷ T_TotalOrder_986 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_f'91'argmin'93''8804'v'8314'_168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_f'91'argmin'93''8804'v'8314'_168 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_f'91'argmin'93''60'v'8314'_178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_f'91'argmin'93''60'v'8314'_178 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_v'8804'f'91'argmin'93''8314'_188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_v'8804'f'91'argmin'93''8314'_188 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_v'60'f'91'argmin'93''8314'_198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_v'60'f'91'argmin'93''8314'_198 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_f'91'argmin'93''8804'f'91''8868''93'_204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_f'91'argmin'93''8804'f'91''8868''93'_204 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_f'91'argmin'93''8804'f'91'xs'93'_216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
du_f'91'argmin'93''8804'f'91'xs'93'_216 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
d_f'91'argmin'93''8776'f'91'v'93''8314'_230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → 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'_230 ∷ T_TotalOrder_986 → (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'_256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → 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'_256 ∷ T_TotalOrder_986 → (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'_284 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → 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'_284 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_argmin'45'sel_300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
du_argmin'45'sel_300 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
d_argmin'45'all_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → (AgdaAny → ()) → AgdaAny → T_All_44 → AgdaAny Source #
du_argmin'45'all_312 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_v'8804'f'91'argmax'93''8314'_374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_v'8804'f'91'argmax'93''8314'_374 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_v'60'f'91'argmax'93''8314'_384 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_v'60'f'91'argmax'93''8314'_384 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_f'91'argmax'93''8804'v'8314'_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_f'91'argmax'93''8804'v'8314'_394 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_f'91'argmax'93''60'v'8314'_404 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_f'91'argmax'93''60'v'8314'_404 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_f'91''8869''93''8804'f'91'argmax'93'_410 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_f'91''8869''93''8804'f'91'argmax'93'_410 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_f'91'xs'93''8804'f'91'argmax'93'_422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
du_f'91'xs'93''8804'f'91'argmax'93'_422 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
d_f'91'argmax'93''8776'f'91'v'93''8314'_436 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → 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'_436 ∷ T_TotalOrder_986 → (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'_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → 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'_462 ∷ T_TotalOrder_986 → (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'_490 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → 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'_490 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_argmax'45'sel_506 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
du_argmax'45'sel_506 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
d_argmax'45'all_518 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_argmax'45'all_518 ∷ T_TotalOrder_986 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_min'8804'v'8314'_572 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_min'8804'v'8314'_572 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_min'60'v'8314'_582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_min'60'v'8314'_582 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_v'8804'min'8314'_592 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_v'8804'min'8314'_592 ∷ T_TotalOrder_986 → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_v'60'min'8314'_602 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_v'60'min'8314'_602 ∷ T_TotalOrder_986 → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_min'8804''8868'_608 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_min'8804'xs_616 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → [AgdaAny] → T_All_44 Source #
du_min'8804'xs_616 ∷ T_TotalOrder_986 → AgdaAny → [AgdaAny] → T_All_44 Source #
d_min'8776'v'8314'_626 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
du_min'8776'v'8314'_626 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
d_min'91'xs'93''8804'min'91'ys'93''8314'_642 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
du_min'91'xs'93''8804'min'91'ys'93''8314'_642 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
d_min'91'xs'93''60'min'91'ys'93''8314'_658 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
du_min'91'xs'93''60'min'91'ys'93''8314'_658 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_min'45'mono'45''8838'_668 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
du_min'45'mono'45''8838'_668 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
d_'46'extendedlambda0_674 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → 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'_684 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_max'8804'v'8314'_684 ∷ T_TotalOrder_986 → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_max'60'v'8314'_694 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_max'60'v'8314'_694 ∷ T_TotalOrder_986 → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_v'8804'max'8314'_704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_v'8804'max'8314'_704 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_v'60'max'8314'_714 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_v'60'max'8314'_714 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_'8869''8804'max_720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_xs'8804'max_728 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → [AgdaAny] → T_All_44 Source #
du_xs'8804'max_728 ∷ T_TotalOrder_986 → AgdaAny → [AgdaAny] → T_All_44 Source #
d_max'8776'v'8314'_738 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
du_max'8776'v'8314'_738 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
d_max'91'xs'93''8804'max'91'ys'93''8314'_754 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
du_max'91'xs'93''8804'max'91'ys'93''8314'_754 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
d_max'91'xs'93''60'max'91'ys'93''8314'_770 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
du_max'91'xs'93''60'max'91'ys'93''8314'_770 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_max'45'mono'45''8838'_780 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
du_max'45'mono'45''8838'_780 ∷ T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
d_'46'extendedlambda1_786 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → T_Any_34 → AgdaAny → T__'8801'__12 → AgdaAny Source #