Documentation

d_map_22 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] Source #

du_map_22 ∷ (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] Source #

d_mapMaybe_32 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → [AgdaAny] Source #

du_mapMaybe_32 ∷ (AgdaAny → Maybe AgdaAny) → [AgdaAny] → [AgdaAny] Source #

d__'43''43'__60 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du__'43''43'__60 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d_intersperse_70 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] Source #

du_intersperse_70 ∷ AgdaAny → [AgdaAny] → [AgdaAny] Source #

d_intercalate_84 ∷ T_Level_18 → () → [AgdaAny] → [[AgdaAny]] → [AgdaAny] Source #

du_intercalate_84 ∷ [AgdaAny] → [[AgdaAny]] → [AgdaAny] Source #

d_cartesianProductWith_98 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du_cartesianProductWith_98 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

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

du_cartesianProduct_110 ∷ [AgdaAny] → [AgdaAny] → [T_Σ_14] Source #

d_alignWith_112 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du_alignWith_112 ∷ (T_These_38 → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d_zipWith_132 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du_zipWith_132 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d_unalignWith_146 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → [AgdaAny] → T_Σ_14 Source #

du_unalignWith_146 ∷ (AgdaAny → T_These_38) → [AgdaAny] → T_Σ_14 Source #

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

du_unzipWith_194 ∷ (AgdaAny → T_Σ_14) → [AgdaAny] → T_Σ_14 Source #

d_partitionSumsWith_204 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T__'8846'__30) → [AgdaAny] → T_Σ_14 Source #

du_partitionSumsWith_204 ∷ (AgdaAny → T__'8846'__30) → [AgdaAny] → T_Σ_14 Source #

d_align_208 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → [AgdaAny] → [T_These_38] Source #

du_align_208 ∷ [AgdaAny] → [AgdaAny] → [T_These_38] Source #

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

du_zip_210 ∷ [AgdaAny] → [AgdaAny] → [T_Σ_14] Source #

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

du_unalign_212 ∷ [T_These_38] → T_Σ_14 Source #

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

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

d_partitionSums_216 ∷ T_Level_18 → () → T_Level_18 → () → [T__'8846'__30] → T_Σ_14 Source #

du_partitionSums_216 ∷ [T__'8846'__30] → T_Σ_14 Source #

d_merge_220 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du_merge_220 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d_foldr_240 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #

du_foldr_240 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #

d_foldl_254 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #

du_foldl_254 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #

d_concat_268 ∷ T_Level_18 → () → [[AgdaAny]] → [AgdaAny] Source #

du_concat_268 ∷ [[AgdaAny]] → [AgdaAny] Source #

d_concatMap_270 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → [AgdaAny] → [AgdaAny] Source #

du_concatMap_270 ∷ (AgdaAny → [AgdaAny]) → [AgdaAny] → [AgdaAny] Source #

d_null_274 ∷ T_Level_18 → () → [AgdaAny] → Bool Source #

du_null_274 ∷ [AgdaAny] → Bool Source #

d_and_280 ∷ [Bool] → Bool Source #

d_or_282 ∷ [Bool] → Bool Source #

d_any_284 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → Bool Source #

du_any_284 ∷ (AgdaAny → Bool) → [AgdaAny] → Bool Source #

d_all_288 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → Bool Source #

du_all_288 ∷ (AgdaAny → Bool) → [AgdaAny] → Bool Source #

d_sum_292 ∷ [Integer] → Integer Source #

d_product_294 ∷ [Integer] → Integer Source #

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

du_length_296 ∷ [AgdaAny] → Integer Source #

d_'91'_'93'_298 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] Source #

du_'91'_'93'_298 ∷ AgdaAny → [AgdaAny] Source #

d_fromMaybe_302 ∷ T_Level_18 → () → Maybe AgdaAny → [AgdaAny] Source #

du_fromMaybe_302 ∷ Maybe AgdaAny → [AgdaAny] Source #

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

du_replicate_306 ∷ Integer → AgdaAny → [AgdaAny] Source #

d_inits_314 ∷ T_Level_18 → () → [AgdaAny] → [[AgdaAny]] Source #

du_inits_314 ∷ [AgdaAny] → [[AgdaAny]] Source #

d_tails_322 ∷ T_Level_18 → () → [AgdaAny] → [[AgdaAny]] Source #

du_tails_322 ∷ [AgdaAny] → [[AgdaAny]] Source #

d_scanr_328 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] Source #

du_scanr_328 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] Source #

d_scanl_366 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] Source #

du_scanl_366 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] Source #

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

du_applyUpTo_380 ∷ (Integer → AgdaAny) → Integer → [AgdaAny] Source #

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

du_applyDownFrom_388 ∷ (Integer → AgdaAny) → Integer → [AgdaAny] Source #

d_tabulate_400 ∷ T_Level_18 → () → Integer → (T_Fin_6 → AgdaAny) → [AgdaAny] Source #

du_tabulate_400 ∷ Integer → (T_Fin_6 → AgdaAny) → [AgdaAny] Source #

d_lookup_410 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_6 → AgdaAny Source #

du_lookup_410 ∷ [AgdaAny] → T_Fin_6 → AgdaAny Source #

d_upTo_422 ∷ Integer → [Integer] Source #

d_downFrom_424 ∷ Integer → [Integer] Source #

d_allFin_428 ∷ Integer → [T_Fin_6] Source #

d_unfold_440 ∷ T_Level_18 → T_Level_18 → () → (Integer → ()) → (Integer → AgdaAny → Maybe T_Σ_14) → Integer → AgdaAny → [AgdaAny] Source #

du_unfold_440 ∷ (Integer → AgdaAny → Maybe T_Σ_14) → Integer → AgdaAny → [AgdaAny] Source #

d_uncons_480 ∷ T_Level_18 → () → [AgdaAny] → Maybe T_Σ_14 Source #

du_uncons_480 ∷ [AgdaAny] → Maybe T_Σ_14 Source #

d_head_486 ∷ T_Level_18 → () → [AgdaAny] → Maybe AgdaAny Source #

du_head_486 ∷ [AgdaAny] → Maybe AgdaAny Source #

d_tail_490 ∷ T_Level_18 → () → [AgdaAny] → Maybe [AgdaAny] Source #

du_tail_490 ∷ [AgdaAny] → Maybe [AgdaAny] Source #

d_last_494 ∷ T_Level_18 → () → [AgdaAny] → Maybe AgdaAny Source #

du_last_494 ∷ [AgdaAny] → Maybe AgdaAny Source #

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

du_take_500 ∷ Integer → [AgdaAny] → [AgdaAny] Source #

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

du_drop_512 ∷ Integer → [AgdaAny] → [AgdaAny] Source #

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

du_splitAt_524 ∷ Integer → [AgdaAny] → T_Σ_14 Source #

d_takeWhile_552 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

du_takeWhile_552 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

d_dropWhile_580 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

du_dropWhile_580 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

d_filter_608 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

du_filter_608 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

d_partition_636 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_Σ_14 Source #

du_partition_636 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → T_Σ_14 Source #

d_span_672 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_Σ_14 Source #

du_span_672 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → T_Σ_14 Source #

d_break_702 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_Σ_14 Source #

du_break_702 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → T_Σ_14 Source #

d_derun_708 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

du_derun_708 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

d_deduplicate_750 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

du_deduplicate_750 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] Source #

d__'91'_'93''37''61'__762 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_6 → (AgdaAny → AgdaAny) → [AgdaAny] Source #

du__'91'_'93''37''61'__762 ∷ [AgdaAny] → T_Fin_6 → (AgdaAny → AgdaAny) → [AgdaAny] Source #

d__'91'_'93''8759''61'__780 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_6 → AgdaAny → [AgdaAny] Source #

du__'91'_'93''8759''61'__780 ∷ [AgdaAny] → T_Fin_6 → AgdaAny → [AgdaAny] Source #

d__'9472'__790 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_6 → [AgdaAny] Source #

du__'9472'__790 ∷ [AgdaAny] → T_Fin_6 → [AgdaAny] Source #

d_reverseAcc_802 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du_reverseAcc_802 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d_reverse_804 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] Source #

du_reverse_804 ∷ [AgdaAny] → [AgdaAny] Source #

d__'691''43''43'__806 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du__'691''43''43'__806 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

d__'8759''691'__808 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → [AgdaAny] Source #

du__'8759''691'__808 ∷ [AgdaAny] → AgdaAny → [AgdaAny] Source #

d__'63''8759'__814 ∷ T_Level_18 → () → Maybe AgdaAny → [AgdaAny] → [AgdaAny] Source #

du__'63''8759'__814 ∷ Maybe AgdaAny → [AgdaAny] → [AgdaAny] Source #

d__'8759''691''63'__816 ∷ T_Level_18 → () → [AgdaAny] → Maybe AgdaAny → [AgdaAny] Source #

du__'8759''691''63'__816 ∷ [AgdaAny] → Maybe AgdaAny → [AgdaAny] Source #

d_InitLast_828 ∷ p → p → p → () Source #

data T_InitLast_828 Source #

d_initLast_842 ∷ T_Level_18 → () → [AgdaAny] → T_InitLast_828 Source #

du_initLast_842 ∷ [AgdaAny] → T_InitLast_828 Source #

d_unsnoc_864 ∷ T_Level_18 → () → [AgdaAny] → Maybe T_Σ_14 Source #

du_unsnoc_864 ∷ [AgdaAny] → Maybe T_Σ_14 Source #

d_linesBy_882 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → [[AgdaAny]] Source #

du_linesBy_882 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → [[AgdaAny]] Source #

d_go_892 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → Maybe [AgdaAny] → [AgdaAny] → [[AgdaAny]] Source #

du_go_892 ∷ (AgdaAny → T_Dec_32) → Maybe [AgdaAny] → [AgdaAny] → [[AgdaAny]] Source #

d_wordsBy_920 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → [[AgdaAny]] Source #

du_wordsBy_920 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → [[AgdaAny]] Source #

d_cons_930 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → [[AgdaAny]] → [[AgdaAny]] Source #

du_cons_930 ∷ [AgdaAny] → [[AgdaAny]] → [[AgdaAny]] Source #

d_go_938 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → [[AgdaAny]] Source #

du_go_938 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → [[AgdaAny]] Source #

d_gfilter_964 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → [AgdaAny] Source #

d_boolFilter_966 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

du_boolFilter_966 ∷ (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

d_boolPartition_972 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

du_boolPartition_972 ∷ (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

d_boolTakeWhile_1006 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

du_boolTakeWhile_1006 ∷ (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

d_boolDropWhile_1032 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

du_boolDropWhile_1032 ∷ (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

d_boolSpan_1058 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

du_boolSpan_1058 ∷ (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

d_boolBreak_1086 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

du_boolBreak_1086 ∷ (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

d__'8759''691'''__1094 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → T_InitLast_828 Source #

du__'8759''691'''__1094 ∷ [AgdaAny] → AgdaAny → T_InitLast_828 Source #