| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Extrema
Documentation
d__'60'__94 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → () Source #
d_argmin_132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_argmin_132 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_argmax_136 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_argmax_136 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_min_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → [AgdaAny] → AgdaAny Source #
du_min_140 ∷ T_TotalOrder_764 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_max_142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → [AgdaAny] → AgdaAny Source #
du_max_142 ∷ T_TotalOrder_764 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_f'91'argmin'93''8804'v'8314'_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_f'91'argmin'93''8804'v'8314'_160 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_f'91'argmin'93''60'v'8314'_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_f'91'argmin'93''60'v'8314'_170 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_v'8804'f'91'argmin'93''8314'_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_v'8804'f'91'argmin'93''8314'_180 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_v'60'f'91'argmin'93''8314'_190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_v'60'f'91'argmin'93''8314'_190 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_f'91'argmin'93''8804'f'91''8868''93'_196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_f'91'argmin'93''8804'f'91''8868''93'_196 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_f'91'argmin'93''8804'f'91'xs'93'_208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
du_f'91'argmin'93''8804'f'91'xs'93'_208 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
d_f'91'argmin'93''8776'f'91'v'93''8314'_222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → 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'_222 ∷ T_TotalOrder_764 → (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'_248 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → 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'_248 ∷ T_TotalOrder_764 → (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'_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → 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'_276 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_argmin'45'sel_292 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
du_argmin'45'sel_292 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
d_argmin'45'all_304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → (AgdaAny → ()) → AgdaAny → T_All_44 → AgdaAny Source #
du_argmin'45'all_304 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_v'8804'f'91'argmax'93''8314'_366 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_v'8804'f'91'argmax'93''8314'_366 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_v'60'f'91'argmax'93''8314'_376 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_v'60'f'91'argmax'93''8314'_376 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_f'91'argmax'93''8804'v'8314'_386 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_f'91'argmax'93''8804'v'8314'_386 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_f'91'argmax'93''60'v'8314'_396 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_f'91'argmax'93''60'v'8314'_396 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_f'91''8869''93''8804'f'91'argmax'93'_402 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
du_f'91''8869''93''8804'f'91'argmax'93'_402 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #
d_f'91'xs'93''8804'f'91'argmax'93'_414 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
du_f'91'xs'93''8804'f'91'argmax'93'_414 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 Source #
d_f'91'argmax'93''8776'f'91'v'93''8314'_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → 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'_428 ∷ T_TotalOrder_764 → (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'_454 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → 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'_454 ∷ T_TotalOrder_764 → (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'_482 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → 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'_482 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_argmax'45'sel_498 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
du_argmax'45'sel_498 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
d_argmax'45'all_510 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_argmax'45'all_510 ∷ T_TotalOrder_764 → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_min'8804'v'8314'_564 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_min'8804'v'8314'_564 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_min'60'v'8314'_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_min'60'v'8314'_574 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_v'8804'min'8314'_584 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_v'8804'min'8314'_584 ∷ T_TotalOrder_764 → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_v'60'min'8314'_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_v'60'min'8314'_594 ∷ T_TotalOrder_764 → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_min'8804''8868'_600 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_min'8804'xs_608 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → [AgdaAny] → T_All_44 Source #
du_min'8804'xs_608 ∷ T_TotalOrder_764 → AgdaAny → [AgdaAny] → T_All_44 Source #
d_min'8776'v'8314'_618 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
du_min'8776'v'8314'_618 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
d_min'91'xs'93''8804'min'91'ys'93''8314'_634 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
du_min'91'xs'93''8804'min'91'ys'93''8314'_634 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
d_min'91'xs'93''60'min'91'ys'93''8314'_650 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
du_min'91'xs'93''60'min'91'ys'93''8314'_650 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_min'45'mono'45''8838'_660 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
du_min'45'mono'45''8838'_660 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
d_'46'extendedlambda0_666 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → 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'_676 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_max'8804'v'8314'_676 ∷ T_TotalOrder_764 → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_max'60'v'8314'_686 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
du_max'60'v'8314'_686 ∷ T_TotalOrder_764 → AgdaAny → [AgdaAny] → T_Σ_14 → T_All_44 → T_Σ_14 Source #
d_v'8804'max'8314'_696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_v'8804'max'8314'_696 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_v'60'max'8314'_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
du_v'60'max'8314'_706 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Σ_14 Source #
d_'8869''8804'max_712 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → [AgdaAny] → AgdaAny Source #
d_xs'8804'max_720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → [AgdaAny] → T_All_44 Source #
du_xs'8804'max_720 ∷ T_TotalOrder_764 → AgdaAny → [AgdaAny] → T_All_44 Source #
d_max'8776'v'8314'_730 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
du_max'8776'v'8314'_730 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_All_44 → AgdaAny → AgdaAny Source #
d_max'91'xs'93''8804'max'91'ys'93''8314'_746 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
du_max'91'xs'93''8804'max'91'ys'93''8314'_746 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → AgdaAny Source #
d_max'91'xs'93''60'max'91'ys'93''8314'_762 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
du_max'91'xs'93''60'max'91'ys'93''8314'_762 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T_All_44 → T_Σ_14 Source #
d_max'45'mono'45''8838'_772 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
du_max'45'mono'45''8838'_772 ∷ T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny Source #
d_'46'extendedlambda1_778 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_764 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → AgdaAny → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → T_Any_34 → AgdaAny → T__'8801'__12 → AgdaAny Source #