Documentation

d_Vec_28 ∷ p → p → p → () Source #

data T_Vec_28 Source #

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

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

d_length_66 ∷ T_Level_18 → () → Integer → T_Vec_28 → Integer Source #

du_length_66 ∷ Integer → Integer Source #

d_head_70 ∷ T_Level_18 → () → Integer → T_Vec_28 → AgdaAny Source #

du_head_70 ∷ T_Vec_28 → AgdaAny Source #

d_tail_76 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Vec_28 Source #

du_tail_76 ∷ T_Vec_28 → T_Vec_28 Source #

d_lookup_82 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Fin_10 → AgdaAny Source #

du_lookup_82 ∷ T_Vec_28 → T_Fin_10 → AgdaAny Source #

d_iterate_96 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → Integer → T_Vec_28 Source #

du_iterate_96 ∷ (AgdaAny → AgdaAny) → AgdaAny → Integer → T_Vec_28 Source #

d_insertAt_108 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Fin_10 → AgdaAny → T_Vec_28 Source #

du_insertAt_108 ∷ T_Vec_28 → T_Fin_10 → AgdaAny → T_Vec_28 Source #

d_removeAt_122 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Fin_10 → T_Vec_28 Source #

du_removeAt_122 ∷ T_Vec_28 → T_Fin_10 → T_Vec_28 Source #

d_updateAt_134 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Fin_10 → (AgdaAny → AgdaAny) → T_Vec_28 Source #

du_updateAt_134 ∷ T_Vec_28 → T_Fin_10 → (AgdaAny → AgdaAny) → T_Vec_28 Source #

d__'91'_'93''37''61'__150 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Fin_10 → (AgdaAny → AgdaAny) → T_Vec_28 Source #

du__'91'_'93''37''61'__150 ∷ T_Vec_28 → T_Fin_10 → (AgdaAny → AgdaAny) → T_Vec_28 Source #

d__'91'_'93''8788'__158 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Fin_10 → AgdaAny → T_Vec_28 Source #

du__'91'_'93''8788'__158 ∷ T_Vec_28 → T_Fin_10 → AgdaAny → T_Vec_28 Source #

d_cast_168 ∷ Integer → Integer → T_Level_18 → () → T__'8801'__12 → T_Vec_28 → T_Vec_28 Source #

du_cast_168 ∷ Integer → T_Vec_28 → T_Vec_28 Source #

d_map_178 ∷ T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → AgdaAny) → T_Vec_28 → T_Vec_28 Source #

du_map_178 ∷ (AgdaAny → AgdaAny) → T_Vec_28 → T_Vec_28 Source #

d__'43''43'__188 ∷ T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du__'43''43'__188 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_concat_198 ∷ T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Vec_28 Source #

du_concat_198 ∷ T_Vec_28 → T_Vec_28 Source #

d_alignWith_204 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → Integer → Integer → (T_These_38 → AgdaAny) → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du_alignWith_204 ∷ (T_These_38 → AgdaAny) → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_restrictWith_224 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → Integer → Integer → (AgdaAny → AgdaAny → AgdaAny) → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du_restrictWith_224 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_zipWith_242 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → AgdaAny → AgdaAny) → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du_zipWith_242 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_unzipWith_256 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → T_Σ_14) → T_Vec_28 → T_Σ_14 Source #

du_unzipWith_256 ∷ (AgdaAny → T_Σ_14) → T_Vec_28 → T_Σ_14 Source #

d_align_266 ∷ T_Level_18 → () → Integer → T_Level_18 → () → Integer → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du_align_266 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_restrict_268 ∷ T_Level_18 → () → Integer → T_Level_18 → () → Integer → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du_restrict_268 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_zip_270 ∷ T_Level_18 → () → Integer → T_Level_18 → () → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du_zip_270 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_unzip_272 ∷ T_Level_18 → () → T_Level_18 → () → Integer → T_Vec_28 → T_Σ_14 Source #

du_unzip_272 ∷ T_Vec_28 → T_Σ_14 Source #

d__'8910'__274 ∷ T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du__'8910'__274 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d__'8859'__284 ∷ T_Level_18 → () → T_Level_18 → () → Integer → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du__'8859'__284 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d__'62''62''61'__296 ∷ T_Level_18 → () → Integer → T_Level_18 → () → Integer → T_Vec_28 → (AgdaAny → T_Vec_28) → T_Vec_28 Source #

du__'62''62''61'__296 ∷ T_Vec_28 → (AgdaAny → T_Vec_28) → T_Vec_28 Source #

d__'8859''42'__302 ∷ T_Level_18 → () → T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du__'8859''42'__302 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_allPairs_310 ∷ T_Level_18 → () → Integer → T_Level_18 → () → Integer → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du_allPairs_310 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_diagonal_316 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Vec_28 Source #

du_diagonal_316 ∷ T_Vec_28 → T_Vec_28 Source #

d__'62''62''61'__324 ∷ T_Level_18 → () → Integer → T_Level_18 → () → T_Vec_28 → (AgdaAny → T_Vec_28) → T_Vec_28 Source #

du__'62''62''61'__324 ∷ T_Vec_28 → (AgdaAny → T_Vec_28) → T_Vec_28 Source #

d_FoldrOp_342 ∷ T_Level_18 → T_Level_18 → () → (Integer → ()) → () Source #

d_FoldlOp_346 ∷ T_Level_18 → T_Level_18 → () → (Integer → ()) → () Source #

d_foldr_352 ∷ T_Level_18 → T_Level_18 → () → Integer → (Integer → ()) → (Integer → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_28 → AgdaAny Source #

du_foldr_352 ∷ Integer → (Integer → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_28 → AgdaAny Source #

d_foldl_372 ∷ T_Level_18 → T_Level_18 → () → Integer → (Integer → ()) → (Integer → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_28 → AgdaAny Source #

du_foldl_372 ∷ (Integer → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_28 → AgdaAny Source #

d_foldr'8242'_390 ∷ T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_28 → AgdaAny Source #

du_foldr'8242'_390 ∷ Integer → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_28 → AgdaAny Source #

d_foldl'8242'_394 ∷ T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_28 → AgdaAny Source #

du_foldl'8242'_394 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Vec_28 → AgdaAny Source #

d_foldr'8321'_398 ∷ T_Level_18 → () → Integer → (AgdaAny → AgdaAny → AgdaAny) → T_Vec_28 → AgdaAny Source #

du_foldr'8321'_398 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec_28 → AgdaAny Source #

d_foldl'8321'_412 ∷ T_Level_18 → () → Integer → (AgdaAny → AgdaAny → AgdaAny) → T_Vec_28 → AgdaAny Source #

du_foldl'8321'_412 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec_28 → AgdaAny Source #

d_sum_420 ∷ Integer → T_Vec_28 → Integer Source #

d_count_424 ∷ T_Level_18 → () → T_Level_18 → Integer → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → T_Vec_28 → Integer Source #

du_count_424 ∷ (AgdaAny → T_Dec_20) → T_Vec_28 → Integer Source #

d_count'7495'_434 ∷ T_Level_18 → () → Integer → (AgdaAny → Bool) → T_Vec_28 → Integer Source #

du_count'7495'_434 ∷ (AgdaAny → Bool) → T_Vec_28 → Integer Source #

d_'91'_'93'_438 ∷ T_Level_18 → () → AgdaAny → T_Vec_28 Source #

du_'91'_'93'_438 ∷ AgdaAny → T_Vec_28 Source #

d_replicate_444 ∷ T_Level_18 → () → Integer → AgdaAny → T_Vec_28 Source #

du_replicate_444 ∷ Integer → AgdaAny → T_Vec_28 Source #

d_tabulate_452 ∷ Integer → T_Level_18 → () → (T_Fin_10 → AgdaAny) → T_Vec_28 Source #

du_tabulate_452 ∷ Integer → (T_Fin_10 → AgdaAny) → T_Vec_28 Source #

d_allFin_462 ∷ Integer → T_Vec_28 Source #

d_splitAt_474 ∷ T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Σ_14 Source #

du_splitAt_474 ∷ Integer → T_Vec_28 → T_Σ_14 Source #

d_take_496 ∷ T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Vec_28 Source #

du_take_496 ∷ Integer → T_Vec_28 → T_Vec_28 Source #

d_drop_506 ∷ T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Vec_28 Source #

du_drop_506 ∷ Integer → T_Vec_28 → T_Vec_28 Source #

d_group_520 ∷ T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Σ_14 Source #

du_group_520 ∷ Integer → Integer → T_Vec_28 → T_Σ_14 Source #

d_split_542 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Σ_14 Source #

du_split_542 ∷ T_Vec_28 → T_Σ_14 Source #

d_uncons_556 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Σ_14 Source #

du_uncons_556 ∷ T_Vec_28 → T_Σ_14 Source #

d_truncate_566 ∷ T_Level_18 → () → Integer → Integer → T__'8804'__22 → T_Vec_28 → T_Vec_28 Source #

du_truncate_566 ∷ Integer → T__'8804'__22 → T_Vec_28 → T_Vec_28 Source #

d_padRight_578 ∷ T_Level_18 → () → Integer → Integer → T__'8804'__22 → AgdaAny → T_Vec_28 → T_Vec_28 Source #

du_padRight_578 ∷ Integer → T__'8804'__22 → AgdaAny → T_Vec_28 → T_Vec_28 Source #

d_toList_592 ∷ T_Level_18 → () → Integer → T_Vec_28 → [AgdaAny] Source #

du_toList_592 ∷ T_Vec_28 → [AgdaAny] Source #

d_fromList_600 ∷ T_Level_18 → () → [AgdaAny] → T_Vec_28 Source #

du_fromList_600 ∷ [AgdaAny] → T_Vec_28 Source #

d__'8759''691'__606 ∷ T_Level_18 → () → Integer → T_Vec_28 → AgdaAny → T_Vec_28 Source #

du__'8759''691'__606 ∷ T_Vec_28 → AgdaAny → T_Vec_28 Source #

d_reverse_616 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Vec_28 Source #

du_reverse_616 ∷ T_Vec_28 → T_Vec_28 Source #

d__'691''43''43'__622 ∷ T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

du__'691''43''43'__622 ∷ T_Vec_28 → T_Vec_28 → T_Vec_28 Source #

d_initLast_640 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Σ_14 Source #

du_initLast_640 ∷ Integer → T_Vec_28 → T_Σ_14 Source #

d_init_658 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Vec_28 Source #

du_init_658 ∷ Integer → T_Vec_28 → T_Vec_28 Source #

d_last_662 ∷ T_Level_18 → () → Integer → T_Vec_28 → AgdaAny Source #

du_last_662 ∷ Integer → T_Vec_28 → AgdaAny Source #

d_transpose_666 ∷ T_Level_18 → () → Integer → Integer → T_Vec_28 → T_Vec_28 Source #

du_transpose_666 ∷ Integer → T_Vec_28 → T_Vec_28 Source #

d_remove_676 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Fin_10 → T_Vec_28 Source #

d_insert_678 ∷ T_Level_18 → () → Integer → T_Vec_28 → T_Fin_10 → AgdaAny → T_Vec_28 Source #