Documentation

d_Vec_24 ∷ p → p → p → () Source #

data T_Vec_24 Source #

d__'91'_'93''61'__44 ∷ p → p → p → p → p → p → () Source #

data T__'91'_'93''61'__44 Source #

d_length_72 ∷ T_Level_18 → () → Integer → T_Vec_24 → Integer Source #

du_length_72 ∷ Integer → Integer Source #

d_head_78 ∷ T_Level_18 → () → Integer → T_Vec_24 → AgdaAny Source #

du_head_78 ∷ T_Vec_24 → AgdaAny Source #

d_tail_86 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Vec_24 Source #

du_tail_86 ∷ T_Vec_24 → T_Vec_24 Source #

d_lookup_94 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Fin_6 → AgdaAny Source #

du_lookup_94 ∷ T_Vec_24 → T_Fin_6 → AgdaAny Source #

d_insert_108 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Fin_6 → AgdaAny → T_Vec_24 Source #

du_insert_108 ∷ T_Vec_24 → T_Fin_6 → AgdaAny → T_Vec_24 Source #

d_remove_124 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Fin_6 → T_Vec_24 Source #

du_remove_124 ∷ T_Vec_24 → T_Fin_6 → T_Vec_24 Source #

d_updateAt_138 ∷ T_Level_18 → () → Integer → T_Fin_6 → (AgdaAny → AgdaAny) → T_Vec_24 → T_Vec_24 Source #

du_updateAt_138 ∷ T_Fin_6 → (AgdaAny → AgdaAny) → T_Vec_24 → T_Vec_24 Source #

d__'91'_'93''37''61'__156 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Fin_6 → (AgdaAny → AgdaAny) → T_Vec_24 Source #

du__'91'_'93''37''61'__156 ∷ T_Vec_24 → T_Fin_6 → (AgdaAny → AgdaAny) → T_Vec_24 Source #

d__'91'_'93''8788'__166 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Fin_6 → AgdaAny → T_Vec_24 Source #

du__'91'_'93''8788'__166 ∷ T_Vec_24 → T_Fin_6 → AgdaAny → T_Vec_24 Source #

d_map_176 ∷ T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → AgdaAny) → T_Vec_24 → T_Vec_24 Source #

du_map_176 ∷ (AgdaAny → AgdaAny) → T_Vec_24 → T_Vec_24 Source #

d__'43''43'__190 ∷ T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du__'43''43'__190 ∷ T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d_concat_204 ∷ T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 Source #

du_concat_204 ∷ T_Vec_24 → T_Vec_24 Source #

d_alignWith_214 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → Integer → Integer → (T_These_38 → AgdaAny) → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du_alignWith_214 ∷ (T_These_38 → AgdaAny) → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d_restrictWith_238 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → Integer → Integer → (AgdaAny → AgdaAny → AgdaAny) → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du_restrictWith_238 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d_zipWith_258 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → AgdaAny → AgdaAny) → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du_zipWith_258 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d_unzipWith_274 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → T_Σ_14) → T_Vec_24 → T_Σ_14 Source #

du_unzipWith_274 ∷ (AgdaAny → T_Σ_14) → T_Vec_24 → T_Σ_14 Source #

d_align_288 ∷ T_Level_18 → () → T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du_align_288 ∷ T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d_restrict_294 ∷ T_Level_18 → () → T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du_restrict_294 ∷ T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d_zip_298 ∷ T_Level_18 → () → T_Level_18 → () → Integer → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du_zip_298 ∷ T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d_unzip_302 ∷ T_Level_18 → () → T_Level_18 → () → Integer → T_Vec_24 → T_Σ_14 Source #

du_unzip_302 ∷ T_Vec_24 → T_Σ_14 Source #

d__'8910'__308 ∷ T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du__'8910'__308 ∷ T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d__'8859'__320 ∷ T_Level_18 → () → T_Level_18 → () → Integer → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du__'8859'__320 ∷ T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d__'62''62''61'__334 ∷ T_Level_18 → () → T_Level_18 → () → Integer → Integer → T_Vec_24 → (AgdaAny → T_Vec_24) → T_Vec_24 Source #

du__'62''62''61'__334 ∷ T_Vec_24 → (AgdaAny → T_Vec_24) → T_Vec_24 Source #

d__'8859''42'__344 ∷ T_Level_18 → () → T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du__'8859''42'__344 ∷ T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d_allPairs_356 ∷ T_Level_18 → () → T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

du_allPairs_356 ∷ T_Vec_24 → T_Vec_24 → T_Vec_24 Source #

d_foldr_374 ∷ T_Level_18 → T_Level_18 → () → (Integer → ()) → Integer → (Integer → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_24 → AgdaAny Source #

du_foldr_374 ∷ Integer → (Integer → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_24 → AgdaAny Source #

d_foldr'8321'_394 ∷ T_Level_18 → () → Integer → (AgdaAny → AgdaAny → AgdaAny) → T_Vec_24 → AgdaAny Source #

du_foldr'8321'_394 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec_24 → AgdaAny Source #

d_foldl_420 ∷ T_Level_18 → T_Level_18 → () → (Integer → ()) → Integer → (Integer → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_24 → AgdaAny Source #

du_foldl_420 ∷ (Integer → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_24 → AgdaAny Source #

d_foldl'8321'_442 ∷ T_Level_18 → () → Integer → (AgdaAny → AgdaAny → AgdaAny) → T_Vec_24 → AgdaAny Source #

du_foldl'8321'_442 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec_24 → AgdaAny Source #

d_sum_452 ∷ Integer → T_Vec_24 → Integer Source #

d_count_458 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → Integer → T_Vec_24 → Integer Source #

du_count_458 ∷ (AgdaAny → T_Dec_32) → T_Vec_24 → Integer Source #

d_'91'_'93'_484 ∷ T_Level_18 → () → AgdaAny → T_Vec_24 Source #

du_'91'_'93'_484 ∷ AgdaAny → T_Vec_24 Source #

d_replicate_490 ∷ T_Level_18 → () → Integer → AgdaAny → T_Vec_24 Source #

du_replicate_490 ∷ Integer → AgdaAny → T_Vec_24 Source #

d_tabulate_500 ∷ T_Level_18 → () → Integer → (T_Fin_6 → AgdaAny) → T_Vec_24 Source #

du_tabulate_500 ∷ Integer → (T_Fin_6 → AgdaAny) → T_Vec_24 Source #

d_allFin_510 ∷ Integer → T_Vec_24 Source #

d_splitAt_522 ∷ T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Σ_14 Source #

du_splitAt_522 ∷ Integer → T_Vec_24 → T_Σ_14 Source #

d_take_548 ∷ T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 Source #

du_take_548 ∷ Integer → T_Vec_24 → T_Vec_24 Source #

d_drop_568 ∷ T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 Source #

du_drop_568 ∷ Integer → T_Vec_24 → T_Vec_24 Source #

d_group_592 ∷ T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Σ_14 Source #

du_group_592 ∷ Integer → Integer → T_Vec_24 → T_Σ_14 Source #

d_split_628 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Σ_14 Source #

du_split_628 ∷ T_Vec_24 → T_Σ_14 Source #

d_uncons_644 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Σ_14 Source #

du_uncons_644 ∷ T_Vec_24 → T_Σ_14 Source #

d_toList_652 ∷ T_Level_18 → () → Integer → T_Vec_24 → [AgdaAny] Source #

du_toList_652 ∷ T_Vec_24 → [AgdaAny] Source #

d_fromList_660 ∷ T_Level_18 → () → [AgdaAny] → T_Vec_24 Source #

du_fromList_660 ∷ [AgdaAny] → T_Vec_24 Source #

d_reverse_668 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Vec_24 Source #

du_reverse_668 ∷ T_Vec_24 → T_Vec_24 Source #

d__'8759''691'__678 ∷ T_Level_18 → () → Integer → T_Vec_24 → AgdaAny → T_Vec_24 Source #

du__'8759''691'__678 ∷ T_Vec_24 → AgdaAny → T_Vec_24 Source #

d_initLast_696 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Σ_14 Source #

du_initLast_696 ∷ Integer → T_Vec_24 → T_Σ_14 Source #

d_init_720 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Vec_24 Source #

du_init_720 ∷ Integer → T_Vec_24 → T_Vec_24 Source #

d_last_734 ∷ T_Level_18 → () → Integer → T_Vec_24 → AgdaAny Source #

du_last_734 ∷ Integer → T_Vec_24 → AgdaAny Source #

d_transpose_750 ∷ T_Level_18 → () → Integer → Integer → T_Vec_24 → T_Vec_24 Source #

du_transpose_750 ∷ Integer → T_Vec_24 → T_Vec_24 Source #