Documentation

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

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

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

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

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

du_intersperse_42 ∷ AgdaAny → [AgdaAny] → [AgdaAny] Source #

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

du_intercalate_56 ∷ [AgdaAny] → [[AgdaAny]] → [AgdaAny] Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

du_unalign_184 ∷ [T_These_38] → T_Σ_14 Source #

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

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

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

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

d_merge_192 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du_merge_192 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

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

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

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

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

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

du_concat_244 ∷ [[AgdaAny]] → [AgdaAny] Source #

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

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

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

du_ap_250 ∷ [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #

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

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

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

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

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

du_null_262 ∷ [AgdaAny] → Bool Source #

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

du_length_268 ∷ [AgdaAny] → Integer Source #

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

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

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

du_fromMaybe_274 ∷ Maybe AgdaAny → [AgdaAny] Source #

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

du_replicate_278 ∷ Integer → AgdaAny → [AgdaAny] Source #

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

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

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

du_inits_298 ∷ [AgdaAny] → [[AgdaAny]] Source #

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

du_tail_304 ∷ [AgdaAny] → [[AgdaAny]] Source #

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

du_tails_314 ∷ [AgdaAny] → [[AgdaAny]] Source #

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

du_tail_320 ∷ [AgdaAny] → [[AgdaAny]] Source #

d_insertAt_328 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → AgdaAny → [AgdaAny] Source #

du_insertAt_328 ∷ [AgdaAny] → T_Fin_10 → AgdaAny → [AgdaAny] Source #

d_updateAt_344 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → (AgdaAny → AgdaAny) → [AgdaAny] Source #

du_updateAt_344 ∷ [AgdaAny] → T_Fin_10 → (AgdaAny → AgdaAny) → [AgdaAny] Source #

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

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

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

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

d_tabulate_380 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → [AgdaAny] Source #

du_tabulate_380 ∷ Integer → (T_Fin_10 → AgdaAny) → [AgdaAny] Source #

d_lookup_390 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → AgdaAny Source #

du_lookup_390 ∷ [AgdaAny] → T_Fin_10 → AgdaAny Source #

d_upTo_402 ∷ Integer → [Integer] Source #

d_downFrom_404 ∷ Integer → [Integer] Source #

d_allFin_408 ∷ Integer → [T_Fin_10] Source #

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

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

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

du_reverseAcc_442 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] Source #

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

du_reverse_444 ∷ [AgdaAny] → [AgdaAny] Source #

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

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

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

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

d_InitLast_458 ∷ p → p → p → () Source #

data T_InitLast_458 Source #

d_initLast_472 ∷ T_Level_18 → () → [AgdaAny] → T_InitLast_458 Source #

du_initLast_472 ∷ [AgdaAny] → T_InitLast_458 Source #

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

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

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

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

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

du_head_516 ∷ [AgdaAny] → Maybe AgdaAny Source #

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

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

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

du_last_524 ∷ [AgdaAny] → Maybe AgdaAny Source #

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

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

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

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

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

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

d_removeAt_570 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → [AgdaAny] Source #

du_removeAt_570 ∷ [AgdaAny] → T_Fin_10 → [AgdaAny] Source #

d_takeWhile_584 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

du_takeWhile_584 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

d_takeWhile'7495'_610 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

du_takeWhile'7495'_610 ∷ (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

d_dropWhile_616 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

du_dropWhile_616 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

d_dropWhile'7495'_642 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

du_dropWhile'7495'_642 ∷ (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

d_filter_648 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

du_filter_648 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

d_filter'7495'_674 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

du_filter'7495'_674 ∷ (AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

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

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

d_partition'7495'_714 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

du_partition'7495'_714 ∷ (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

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

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

d_span'7495'_754 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

du_span'7495'_754 ∷ (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

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

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

d_break'7495'_764 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

du_break'7495'_764 ∷ (AgdaAny → Bool) → [AgdaAny] → T_Σ_14 Source #

d_linesBy_770 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → [[AgdaAny]] Source #

du_linesBy_770 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → [[AgdaAny]] Source #

d_go_780 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → Maybe [AgdaAny] → [AgdaAny] → [[AgdaAny]] Source #

du_go_780 ∷ (AgdaAny → T_Dec_20) → Maybe [AgdaAny] → [AgdaAny] → [[AgdaAny]] Source #

d_acc'8242'_794 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → Maybe [AgdaAny] → AgdaAny → [AgdaAny] → [AgdaAny] Source #

du_acc'8242'_794 ∷ Maybe [AgdaAny] → [AgdaAny] Source #

d_linesBy'7495'_796 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → [[AgdaAny]] Source #

du_linesBy'7495'_796 ∷ (AgdaAny → Bool) → [AgdaAny] → [[AgdaAny]] Source #

d_wordsBy_802 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → [[AgdaAny]] Source #

du_wordsBy_802 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → [[AgdaAny]] Source #

d_cons_812 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → [[AgdaAny]] → [[AgdaAny]] Source #

du_cons_812 ∷ [AgdaAny] → [[AgdaAny]] → [[AgdaAny]] Source #

d_go_820 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → [[AgdaAny]] Source #

du_go_820 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → [[AgdaAny]] Source #

d_wordsBy'7495'_830 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → [[AgdaAny]] Source #

du_wordsBy'7495'_830 ∷ (AgdaAny → Bool) → [AgdaAny] → [[AgdaAny]] Source #

d_derun_836 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

du_derun_836 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

d_derun'7495'_876 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

du_derun'7495'_876 ∷ (AgdaAny → AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

d_deduplicate_882 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

du_deduplicate_882 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] Source #

d_deduplicate'7495'_892 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

du_deduplicate'7495'_892 ∷ (AgdaAny → AgdaAny → Bool) → [AgdaAny] → [AgdaAny] Source #

d_find_898 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → Maybe AgdaAny Source #

du_find_898 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → Maybe AgdaAny Source #

d_find'7495'_908 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → Maybe AgdaAny Source #

du_find'7495'_908 ∷ (AgdaAny → Bool) → [AgdaAny] → Maybe AgdaAny Source #

d_findIndex_916 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → Maybe T_Fin_10 Source #

du_findIndex_916 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → Maybe T_Fin_10 Source #

d_findIndex'7495'_928 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → Maybe T_Fin_10 Source #

du_findIndex'7495'_928 ∷ (AgdaAny → Bool) → [AgdaAny] → Maybe T_Fin_10 Source #

d_findIndices_936 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → [T_Fin_10] Source #

du_findIndices_936 ∷ T_Level_18 → T_Level_18 → (AgdaAny → T_Dec_20) → [AgdaAny] → [T_Fin_10] Source #

d_indices_950 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → [T_Fin_10] Source #

du_indices_950 ∷ T_Level_18 → T_Level_18 → (AgdaAny → T_Dec_20) → [AgdaAny] → [T_Fin_10] Source #

d_findIndices'7495'_954 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → [T_Fin_10] Source #

du_findIndices'7495'_954 ∷ T_Level_18 → (AgdaAny → Bool) → [AgdaAny] → [T_Fin_10] Source #

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

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

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

du__'91'_'93''8759''61'__970 ∷ [AgdaAny] → T_Fin_10 → AgdaAny → [AgdaAny] Source #

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

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

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

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

d_'43''43''45'rawMagma_996 ∷ T_Level_18 → () → T_RawMagma_44 Source #

du_'43''43''45'rawMagma_996 ∷ T_RawMagma_44 Source #

d_'43''43''45''91''93''45'rawMonoid_998 ∷ T_Level_18 → () → T_RawMonoid_74 Source #

du_'43''43''45''91''93''45'rawMonoid_998 ∷ T_RawMonoid_74 Source #

d__'8759''691'''__1004 ∷ [AgdaAny] → AgdaAny → T_InitLast_458 Source #

d__'9472'__1006 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → [AgdaAny] Source #

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

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

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

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

d_and_1060 ∷ [Bool] → Bool Source #

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

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

d_or_1066 ∷ [Bool] → Bool Source #

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

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

d_sum_1072 ∷ [Integer] → Integer Source #

d_product_1074 ∷ [Integer] → Integer Source #