Documentation

d_max_50 ∷ Integer → [Integer] → Integer Source #

d_xs'8804'max_98 ∷ Integer → [Integer] → T_All_44 Source #

d_Vec'8804'_122 ∷ p → p → p → () Source #

data T_Vec'8804'_122 Source #

d_length_134 ∷ T_Vec'8804'_122 → Integer Source #

d_vec_136 ∷ T_Vec'8804'_122 → T_Vec_24 Source #

d_fromVec_144 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_Vec'8804'_122 Source #

du_fromVec_144 ∷ Integer → T_Vec_24 → T_Vec'8804'_122 Source #

d_padRight_150 ∷ T_Level_18 → () → Integer → AgdaAny → T_Vec'8804'_122 → T_Vec_24 Source #

du_padRight_150 ∷ Integer → AgdaAny → T_Vec'8804'_122 → T_Vec_24 Source #

d_padLeft_170 ∷ T_Level_18 → () → Integer → AgdaAny → T_Vec'8804'_122 → T_Vec_24 Source #

du_padLeft_170 ∷ Integer → AgdaAny → T_Vec'8804'_122 → T_Vec_24 Source #

d_split_218 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #

d_padBoth_238 ∷ T_Level_18 → () → Integer → AgdaAny → AgdaAny → T_Vec'8804'_122 → T_Vec_24 Source #

du_padBoth_238 ∷ Integer → AgdaAny → AgdaAny → T_Vec'8804'_122 → T_Vec_24 Source #

d_fromList_288 ∷ T_Level_18 → () → [AgdaAny] → T_Vec'8804'_122 Source #

du_fromList_288 ∷ [AgdaAny] → T_Vec'8804'_122 Source #

d_toList_292 ∷ T_Level_18 → () → Integer → T_Vec'8804'_122 → [AgdaAny] Source #

du_toList_292 ∷ T_Vec'8804'_122 → [AgdaAny] Source #

d_replicate_300 ∷ T_Level_18 → () → Integer → Integer → T__'8804'__18 → AgdaAny → T_Vec'8804'_122 Source #

du_replicate_300 ∷ Integer → AgdaAny → T_Vec'8804'_122 Source #

d_'91''93'_308 ∷ T_Level_18 → () → Integer → T_Vec'8804'_122 Source #

du_'91''93'_308 ∷ T_Vec'8804'_122 Source #

d__'8759'__312 ∷ T_Level_18 → () → Integer → AgdaAny → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du__'8759'__312 ∷ AgdaAny → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_'8804''45'cast_326 ∷ T_Level_18 → () → Integer → Integer → T__'8804'__18 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_'8804''45'cast_326 ∷ T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_'8801''45'cast_340 ∷ T_Level_18 → () → Integer → Integer → T__'8801'__12 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_'8801''45'cast_340 ∷ T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_map_346 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Integer → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_map_346 ∷ (AgdaAny → AgdaAny) → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_reverse_356 ∷ T_Level_18 → () → Integer → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_reverse_356 ∷ T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_alignWith_364 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → Integer → T_Vec'8804'_122 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_alignWith_364 ∷ (T_These_38 → AgdaAny) → T_Vec'8804'_122 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_zipWith_378 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → Integer → T_Vec'8804'_122 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_zipWith_378 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_Vec'8804'_122 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_zip_392 ∷ T_Level_18 → () → T_Level_18 → () → Integer → T_Vec'8804'_122 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_zip_392 ∷ T_Vec'8804'_122 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_align_396 ∷ T_Level_18 → () → T_Level_18 → () → Integer → T_Vec'8804'_122 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_align_396 ∷ T_Vec'8804'_122 → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_take_402 ∷ T_Level_18 → () → Integer → Integer → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_take_402 ∷ Integer → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

d_drop_422 ∷ T_Level_18 → () → Integer → Integer → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

du_drop_422 ∷ Integer → T_Vec'8804'_122 → T_Vec'8804'_122 Source #

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

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

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

du_sizes_450 ∷ [T_Σ_14] → [Integer] Source #

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

du_width_452 ∷ [T_Σ_14] → Integer Source #

d_all'8804'_456 ∷ T_Level_18 → () → [T_Σ_14] → T_All_44 Source #

du_all'8804'_456 ∷ [T_Σ_14] → T_All_44 Source #

d_padded_458 ∷ T_Level_18 → () → [T_Σ_14] → [T_Vec'8804'_122] Source #

du_padded_458 ∷ [T_Σ_14] → [T_Vec'8804'_122] Source #