Documentation

d_List'8314'_24 ∷ p → p → () Source #

data T_List'8314'_24 Source #

d_head_32 ∷ T_List'8314'_24 → AgdaAny Source #

d_tail_34 ∷ T_List'8314'_24 → [AgdaAny] Source #

d_uncons_38 ∷ T_Level_18 → () → T_List'8314'_24 → T_Σ_14 Source #

du_uncons_38 ∷ T_List'8314'_24 → T_Σ_14 Source #

d_'91'_'93'_44 ∷ T_Level_18 → () → AgdaAny → T_List'8314'_24 Source #

du_'91'_'93'_44 ∷ AgdaAny → T_List'8314'_24 Source #

d__'8759''8314'__48 ∷ T_Level_18 → () → AgdaAny → T_List'8314'_24 → T_List'8314'_24 Source #

du__'8759''8314'__48 ∷ AgdaAny → T_List'8314'_24 → T_List'8314'_24 Source #

d_length_56 ∷ T_Level_18 → () → T_List'8314'_24 → Integer Source #

du_length_56 ∷ T_List'8314'_24 → Integer Source #

d_toList_62 ∷ T_Level_18 → () → T_List'8314'_24 → [AgdaAny] Source #

du_toList_62 ∷ T_List'8314'_24 → [AgdaAny] Source #

d_fromList_68 ∷ T_Level_18 → () → [AgdaAny] → Maybe T_List'8314'_24 Source #

du_fromList_68 ∷ [AgdaAny] → Maybe T_List'8314'_24 Source #

d_fromVec_76 ∷ T_Level_18 → () → Integer → T_Vec_24 → T_List'8314'_24 Source #

du_fromVec_76 ∷ T_Vec_24 → T_List'8314'_24 Source #

d_toVec_84 ∷ T_Level_18 → () → T_List'8314'_24 → T_Vec_24 Source #

du_toVec_84 ∷ T_List'8314'_24 → T_Vec_24 Source #

d_lift_94 ∷ T_Level_18 → () → T_Level_18 → () → (Integer → T_Vec_24 → T_Σ_14) → T_List'8314'_24 → T_List'8314'_24 Source #

du_lift_94 ∷ (Integer → T_Vec_24 → T_Σ_14) → T_List'8314'_24 → T_List'8314'_24 Source #

d_map_100 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_List'8314'_24 → T_List'8314'_24 Source #

du_map_100 ∷ (AgdaAny → AgdaAny) → T_List'8314'_24 → T_List'8314'_24 Source #

d_replicate_110 ∷ T_Level_18 → () → Integer → (T__'8801'__12 → T_'8869'_4) → AgdaAny → T_List'8314'_24 Source #

du_replicate_110 ∷ Integer → AgdaAny → T_List'8314'_24 Source #

d_foldr_118 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_List'8314'_24 → AgdaAny Source #

du_foldr_118 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_List'8314'_24 → AgdaAny Source #

d_foldr'8242'_136 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → [AgdaAny] → AgdaAny Source #

du_foldr'8242'_136 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny Source #

d_foldr'8321'_146 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_List'8314'_24 → AgdaAny Source #

du_foldr'8321'_146 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_List'8314'_24 → AgdaAny Source #

d_foldl_150 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_List'8314'_24 → AgdaAny Source #

du_foldl_150 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_List'8314'_24 → AgdaAny Source #

d_foldl'8321'_160 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_List'8314'_24 → AgdaAny Source #

du_foldl'8321'_160 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_List'8314'_24 → AgdaAny Source #

d__'8314''43''43''8314'__164 ∷ T_Level_18 → () → T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

du__'8314''43''43''8314'__164 ∷ T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

d__'8314''43''43'__174 ∷ T_Level_18 → () → T_List'8314'_24 → [AgdaAny] → T_List'8314'_24 Source #

du__'8314''43''43'__174 ∷ T_List'8314'_24 → [AgdaAny] → T_List'8314'_24 Source #

d__'43''43''8314'__182 ∷ T_Level_18 → () → [AgdaAny] → T_List'8314'_24 → T_List'8314'_24 Source #

du__'43''43''8314'__182 ∷ [AgdaAny] → T_List'8314'_24 → T_List'8314'_24 Source #

d_concat_188 ∷ T_Level_18 → () → T_List'8314'_24 → T_List'8314'_24 Source #

du_concat_188 ∷ T_List'8314'_24 → T_List'8314'_24 Source #

d_concatMap_194 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_List'8314'_24) → T_List'8314'_24 → T_List'8314'_24 Source #

du_concatMap_194 ∷ (AgdaAny → T_List'8314'_24) → T_List'8314'_24 → T_List'8314'_24 Source #

d_reverse_198 ∷ T_Level_18 → () → T_List'8314'_24 → T_List'8314'_24 Source #

du_reverse_198 ∷ T_List'8314'_24 → T_List'8314'_24 Source #

d_alignWith_200 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

du_alignWith_200 ∷ (T_These_38 → AgdaAny) → T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

d_zipWith_212 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

du_zipWith_212 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

d_unalignWith_224 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → T_List'8314'_24 → T_These_38 Source #

du_unalignWith_224 ∷ (AgdaAny → T_These_38) → T_List'8314'_24 → T_These_38 Source #

d_mcons_236 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → T_Level_18 → () → T_These_38 → T_List'8314'_24 Source #

du_mcons_236 ∷ T_These_38 → T_List'8314'_24 Source #

d_unzipWith_238 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → T_List'8314'_24 → T_Σ_14 Source #

du_unzipWith_238 ∷ (AgdaAny → T_Σ_14) → T_List'8314'_24 → T_Σ_14 Source #

d_align_246 ∷ T_Level_18 → () → T_Level_18 → () → T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

du_align_246 ∷ T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

d_zip_248 ∷ T_Level_18 → () → T_Level_18 → () → T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

du_zip_248 ∷ T_List'8314'_24 → T_List'8314'_24 → T_List'8314'_24 Source #

d_unalign_250 ∷ T_Level_18 → () → T_Level_18 → () → T_List'8314'_24 → T_These_38 Source #

du_unalign_250 ∷ T_List'8314'_24 → T_These_38 Source #

d_unzip_252 ∷ T_Level_18 → () → T_Level_18 → () → T_List'8314'_24 → T_Σ_14 Source #

du_unzip_252 ∷ T_List'8314'_24 → T_Σ_14 Source #

d__'8759''691'__254 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → T_List'8314'_24 Source #

du__'8759''691'__254 ∷ [AgdaAny] → AgdaAny → T_List'8314'_24 Source #

d__'8314''8759''691'__264 ∷ T_Level_18 → () → T_List'8314'_24 → AgdaAny → T_List'8314'_24 Source #

du__'8314''8759''691'__264 ∷ T_List'8314'_24 → AgdaAny → T_List'8314'_24 Source #

d_SnocView_274 ∷ p → p → p → () Source #

data T_SnocView_274 Source #

d_snocView_286 ∷ T_Level_18 → () → T_List'8314'_24 → T_SnocView_274 Source #

du_snocView_286 ∷ T_List'8314'_24 → T_SnocView_274 Source #

d_last_304 ∷ T_Level_18 → () → T_List'8314'_24 → AgdaAny Source #

du_last_304 ∷ T_List'8314'_24 → AgdaAny Source #