| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Properties
Documentation
d_'8759''45'injective_42 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Σ_14 Source #
d_'8759''45'injective'737'_44 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'8759''45'injective'691'_46 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'8759''45'dec_48 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Dec_32 → T_Dec_32 → T_Dec_32 Source #
d_'8801''45'dec_54 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → T_Dec_32 Source #
d_map'45'id_80 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_map'45'id'8322'_94 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_map'45''43''43''45'commute_106 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45'cong_126 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'cong'8322'_144 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_length'45'map_154 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'compose_168 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'injective_178 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_mapMaybe'45'just_202 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybe'45'nothing_214 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybe'45'concatMap_230 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'mapMaybe_254 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → T__'8804'__18 Source #
du_length'45'mapMaybe_254 ∷ (AgdaAny → Maybe AgdaAny) → [AgdaAny] → T__'8804'__18 Source #
d_length'45''43''43'_278 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_Associative_312 ∷ T_Level_18 → () → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_Cancellative_314 ∷ T_Level_18 → () → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_Conical_322 ∷ T_Level_18 → () → [AgdaAny] → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_Identity_328 ∷ T_Level_18 → () → [AgdaAny] → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_LeftIdentity_342 ∷ T_Level_18 → () → [AgdaAny] → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_RightIdentity_354 ∷ T_Level_18 → () → [AgdaAny] → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_IsMagma_396 ∷ p → p → p → () Source #
d_IsMonoid_398 ∷ p → p → p → p → () Source #
d_IsSemigroup_406 ∷ p → p → p → () Source #
d_'43''43''45'assoc_1788 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_'43''43''45'identity'737'_1804 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_'43''43''45'identity'691'_1808 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_'43''43''45'identity_1816 ∷ T_Level_18 → () → T_Σ_14 Source #
d_'43''43''45'identity'691''45'unique_1822 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'identity'737''45'unique_1834 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'cancel'737'_1872 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'cancel'691'_1888 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'cancel_1916 ∷ T_Level_18 → () → T_Σ_14 Source #
d_'43''43''45'conical'737'_1922 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'conical'691'_1928 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'conical_1930 ∷ T_Level_18 → () → T_Σ_14 Source #
d_alignWith'45'cong_1966 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → (T_These_38 → AgdaAny) → (T_These_38 → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_length'45'alignWith_1990 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → (T_These_38 → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_alignWith'45'map_2012 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → (T_These_38 → AgdaAny) → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45'alignWith_2044 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → (T_These_38 → AgdaAny) → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'comm_2082 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'identity'737'_2122 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'identity'691'_2130 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'zipWith_2140 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'map_2178 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45'zipWith_2226 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'this_2254 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'that_2264 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'cong_2286 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → (AgdaAny → T_These_38) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'map_2350 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'unalignWith_2402 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'alignWith_2466 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → (T_These_38 → AgdaAny) → (T_These_38 → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_length'45'unzipWith'8321'_2514 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'unzipWith'8322'_2522 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'unzipWith_2530 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45'universal_2554 ∷ T_Level_18 → () → T_Level_18 → () → ([AgdaAny] → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T__'8801'__12 → (AgdaAny → [AgdaAny] → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45'cong_2592 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → T__'8801'__12) → T__'8801'__12 → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45'fusion_2620 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_id'45'is'45'foldr_2636 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_'43''43''45'is'45'foldr_2646 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45''43''43'_2668 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45'is'45'foldr_2692 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45''8759''691'_2714 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45'forces'7495'_2752 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → T_Σ_14) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 Source #
du_foldr'45'forces'7495'_2752 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → T_Σ_14) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 Source #
d_foldr'45'preserves'7495'_2786 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_foldr'45'preserves'7495'_2786 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_foldr'45'preserves'691'_2806 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny Source #
du_foldr'45'preserves'691'_2806 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny Source #
d_foldr'45'preserves'7506'_2826 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30 → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_foldr'45'preserves'7506'_2826 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30 → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_foldl'45''43''43'_2872 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_foldl'45''8759''691'_2898 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_concat'45'map_2918 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [[AgdaAny]] → T__'8801'__12 Source #
d_concat'45''43''43'_2940 ∷ T_Level_18 → () → [[AgdaAny]] → [[AgdaAny]] → T__'8801'__12 Source #
d_concat'45'concat_2958 ∷ T_Level_18 → () → [[[AgdaAny]]] → T__'8801'__12 Source #
d_concat'45''91''45''93'_2966 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_length'45'replicate_2994 ∷ T_Level_18 → () → Integer → AgdaAny → T__'8801'__12 Source #
d_scanr'45'defn_3002 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_scanl'45'defn_3084 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_length'45'applyUpTo_3108 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_lookup'45'applyUpTo_3122 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T_Fin_6 → T__'8801'__12 Source #
d_length'45'applyDownFrom_3144 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_lookup'45'applyDownFrom_3152 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T_Fin_6 → T__'8801'__12 Source #
d_tabulate'45'cong_3186 ∷ T_Level_18 → () → Integer → (T_Fin_6 → AgdaAny) → (T_Fin_6 → AgdaAny) → (T_Fin_6 → T__'8801'__12) → T__'8801'__12 Source #
d_tabulate'45'lookup_3196 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_length'45'tabulate_3208 ∷ T_Level_18 → () → Integer → (T_Fin_6 → AgdaAny) → T__'8801'__12 Source #
d_lookup'45'tabulate_3226 ∷ T_Level_18 → () → Integer → (T_Fin_6 → AgdaAny) → T_Fin_6 → T__'8801'__12 Source #
d_map'45'tabulate_3240 ∷ T_Level_18 → () → T_Level_18 → () → Integer → (T_Fin_6 → AgdaAny) → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_length'45''37''61'_3260 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_6 → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_length'45''8759''61'_3282 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_6 → AgdaAny → T__'8801'__12 Source #
d_map'45''8759''61'_3300 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T_Fin_6 → AgdaAny → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_length'45''9472'_3326 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_6 → T__'8801'__12 Source #
d_map'45''9472'_3348 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T_Fin_6 → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_length'45'take_3370 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8801'__12 Source #
d_length'45'drop_3386 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8801'__12 Source #
d_take'43''43'drop_3402 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8801'__12 Source #
d_splitAt'45'defn_3418 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8801'__12 Source #
d_takeWhile'43''43'dropWhile_3462 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T__'8801'__12 Source #
d_span'45'defn_3482 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'filter_3516 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T__'8804'__18 Source #
du_length'45'filter_3516 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → T__'8804'__18 Source #
d_filter'45'all_3536 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_filter'45'notAll_3572 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_Any_34 → T__'8804'__18 Source #
du_filter'45'notAll_3572 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → T_Any_34 → T__'8804'__18 Source #
d_filter'45'some_3622 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_Any_34 → T__'8804'__18 Source #
du_filter'45'some_3622 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → T_Any_34 → T__'8804'__18 Source #
d_filter'45'none_3672 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_filter'45'complete_3706 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_filter'45'accept_3738 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → AgdaAny → [AgdaAny] → AgdaAny → T__'8801'__12 Source #
d_filter'45'reject_3762 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → AgdaAny → [AgdaAny] → (AgdaAny → T_'8869'_4) → T__'8801'__12 Source #
d_filter'45'idem_3782 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T__'8801'__12 Source #
d_filter'45''43''43'_3812 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_length'45'derun_3854 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → T__'8804'__18 Source #
du_length'45'derun_3854 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → T__'8804'__18 Source #
d_length'45'deduplicate_3886 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → T__'8804'__18 Source #
du_length'45'deduplicate_3886 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → T__'8804'__18 Source #
d_r_3896 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → [AgdaAny] → [AgdaAny] Source #
d_derun'45'reject_3904 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T__'8801'__12 Source #
d_derun'45'accept_3942 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → [AgdaAny] → (AgdaAny → T_'8869'_4) → T__'8801'__12 Source #
d_partition'45'defn_3986 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'partition_4014 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_Σ_14 Source #
d_'691''43''43''45'defn_4040 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_'691''43''43''45''43''43'_4056 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_'691''43''43''45''691''43''43'_4072 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_length'45''691''43''43'_4086 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45''691''43''43'_4100 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45''691''43''43'_4120 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_foldl'45''691''43''43'_4144 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_unfold'45'reverse_4164 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45''43''43''45'commute_4174 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'involutive_4180 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'injective_4188 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_length'45'reverse_4192 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'map'45'commute_4198 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'foldr_4208 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'foldl_4222 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_'8759''691''45'injective_4244 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Σ_14 Source #
d_'8759''691''45'injective'737'_4278 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'8759''691''45'injective'691'_4290 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_gfilter'45'just_4298 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_gfilter'45'nothing_4300 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_gfilter'45'concatMap_4302 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'gfilter_4304 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → T__'8804'__18 Source #
d_right'45'identity'45'unique_4306 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_left'45'identity'45'unique_4308 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_boolTakeWhile'43''43'boolDropWhile_4320 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T__'8801'__12 Source #
d_boolSpan'45'defn_4340 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'boolFilter_4362 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T__'8804'__18 Source #
du_length'45'boolFilter_4362 ∷ (AgdaAny → Bool) → [AgdaAny] → T__'8804'__18 Source #
d_boolPartition'45'defn_4368 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T__'8801'__12 Source #
d_boolFilter'45'filters_4404 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_All_44 Source #
d_idIsFold_4424 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_'43''43'IsFold_4426 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_mapIsFold_4428 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #