| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Properties
Documentation
d_'8759''45'injective_48 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → [AgdaAny] → T__'8801'__12 → T_Σ_14 Source #
d_'8759''45'injective'737'_50 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'8759''45'injective'691'_52 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'8759''45'dec_54 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Dec_20 → T_Dec_20 → T_Dec_20 Source #
d_'8801''45'dec_60 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Dec_20 Source #
d_map'45'id_86 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_map'45'id'45'local_100 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_map'45''43''43'_112 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45'cong_132 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'cong'45'local_150 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_length'45'map_160 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45''8728'_174 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'injective_184 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_length'45''43''43'_210 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_Associative_248 ∷ T_Level_18 → () → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_Cancellative_250 ∷ T_Level_18 → () → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_Conical_258 ∷ T_Level_18 → () → [AgdaAny] → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_Identity_268 ∷ T_Level_18 → () → [AgdaAny] → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_LeftCancellative_282 ∷ T_Level_18 → () → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_LeftIdentity_294 ∷ T_Level_18 → () → [AgdaAny] → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_RightCancellative_312 ∷ T_Level_18 → () → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_RightIdentity_324 ∷ T_Level_18 → () → [AgdaAny] → ([AgdaAny] → [AgdaAny] → [AgdaAny]) → () Source #
d_'43''43''45'assoc_354 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_'43''43''45'identity'737'_370 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_'43''43''45'identity'691'_374 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_'43''43''45'identity_382 ∷ T_Level_18 → () → T_Σ_14 Source #
d_'43''43''45'identity'691''45'unique_388 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'identity'737''45'unique_400 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'cancel'737'_432 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'cancel'691'_442 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'cancel_470 ∷ T_Level_18 → () → T_Σ_14 Source #
d_'43''43''45'conical'737'_476 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'conical'691'_482 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'43''43''45'conical_484 ∷ T_Level_18 → () → T_Σ_14 Source #
d_length'45''43''43''45'suc'737'_492 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_length'45''43''43''45'suc'691'_500 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_length'45''43''43''45'comm_512 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_length'45''43''43''45''8804''737'_532 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8804'__22 Source #
d_length'45''43''43''45''8804''691'_542 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8804'__22 Source #
d_IsMagma_646 ∷ p → p → p → () Source #
d_IsMonoid_658 ∷ p → p → p → p → () Source #
d_IsSemigroup_702 ∷ p → p → p → () Source #
d_'8729''45'cong_2012 ∷ T_IsMagma_178 → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_assoc_2854 ∷ T_IsSemigroup_488 → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_prod_3224 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] Source #
d_cartesianProductWith'45'zero'737'_3228 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_cartesianProductWith'45'zero'691'_3232 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_cartesianProductWith'45'distrib'691''45''43''43'_3244 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_alignWith'45'cong_3276 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → (T_These_38 → AgdaAny) → (T_These_38 → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_length'45'alignWith_3312 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_alignWith'45'map_3334 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45'alignWith_3366 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_alignWith'45'flip_3390 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_alignWith'45'comm_3424 ∷ T_Level_18 → () → T_Level_18 → () → (T_These_38 → AgdaAny) → (T_These_38 → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_align'45'map_3440 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_align'45'flip_3454 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'cong_3480 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'zero'737'_3514 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'zero'691'_3522 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'zipWith_3532 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'map_3562 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45'zipWith_3606 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'flip_3636 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'comm_3674 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zip'45'map_3690 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zip'45'flip_3708 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'this_3716 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'that_3726 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'cong_3748 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → (AgdaAny → T_These_38) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'map_3812 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'unalignWith_3864 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_unalignWith'45'alignWith_3928 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_These_38) → (T_These_38 → AgdaAny) → (T_These_38 → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_unzipWith'45'cong_3976 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → (AgdaAny → T_Σ_14) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'unzipWith'8321'_4000 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'unzipWith'8322'_4008 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'unzipWith_4016 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_unzipWith'45'zipWith_4036 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → (AgdaAny → AgdaAny → AgdaAny) → (T_Σ_14 → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_unzipWith'45'map_4060 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'unzipWith_4074 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_unzipWith'45'swap_4088 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → [AgdaAny] → T__'8801'__12 Source #
d_unzipWith'45''43''43'_4098 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T_Σ_14) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_unzip'45'map_4112 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [T_Σ_14] → T__'8801'__12 Source #
d_unzip'45'swap_4120 ∷ T_Level_18 → () → T_Level_18 → () → [T_Σ_14] → T__'8801'__12 Source #
d_zip'45'unzip_4124 ∷ T_Level_18 → () → T_Level_18 → () → [T_Σ_14] → T__'8801'__12 Source #
d_unzip'45'zip_4132 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_foldr'45'universal_4146 ∷ T_Level_18 → () → T_Level_18 → () → ([AgdaAny] → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T__'8801'__12 → (AgdaAny → [AgdaAny] → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45'cong_4184 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → T__'8801'__12) → T__'8801'__12 → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45'fusion_4212 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_id'45'is'45'foldr_4228 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_'43''43''45'is'45'foldr_4238 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45''43''43'_4260 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45'is'45'foldr_4284 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45''8759''691'_4306 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45'map_4332 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45'forces'7495'_4370 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → T_Σ_14) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 Source #
du_foldr'45'forces'7495'_4370 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → T_Σ_14) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 Source #
d_foldr'45'preserves'7495'_4392 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
du_foldr'45'preserves'7495'_4392 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny Source #
d_foldr'45'preserves'691'_4412 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny Source #
du_foldr'45'preserves'691'_4412 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny Source #
d_foldr'45'preserves'7506'_4432 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30 → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
du_foldr'45'preserves'7506'_4432 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30 → AgdaAny) → AgdaAny → [AgdaAny] → T__'8846'__30 → AgdaAny Source #
d_foldl'45'cong_4480 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_foldl'45''43''43'_4506 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_foldl'45''8759''691'_4532 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_foldl'45'map_4558 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_concat'45'map_4578 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [[AgdaAny]] → T__'8801'__12 Source #
d_concat'45''43''43'_4600 ∷ T_Level_18 → () → [[AgdaAny]] → [[AgdaAny]] → T__'8801'__12 Source #
d_concat'45'concat_4618 ∷ T_Level_18 → () → [[[AgdaAny]]] → T__'8801'__12 Source #
d_concat'45'map'45''91'_'93'_4626 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_concat'45''91'_'93'_4634 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_concatMap'45'cong_4642 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → (AgdaAny → [AgdaAny]) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_concatMap'45'pure_4646 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_concatMap'45'map_4652 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'concatMap_4662 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → [AgdaAny]) → [AgdaAny] → T__'8801'__12 Source #
d_concatMap'45''43''43'_4676 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_catMaybes'45'concatMap_4688 ∷ T_Level_18 → () → [Maybe AgdaAny] → T__'8801'__12 Source #
d_length'45'catMaybes_4700 ∷ T_Level_18 → () → [Maybe AgdaAny] → T__'8804'__22 Source #
d_catMaybes'45''43''43'_4710 ∷ T_Level_18 → () → [Maybe AgdaAny] → [Maybe AgdaAny] → T__'8801'__12 Source #
d_map'45'catMaybes_4726 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [Maybe AgdaAny] → T__'8801'__12 Source #
d_Any'45'catMaybes'8314'_4744 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [Maybe AgdaAny] → T_Any_34 → T_Any_34 Source #
d_mapMaybe'45'cong_4766 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → (AgdaAny → Maybe AgdaAny) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybe'45'just_4772 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybe'45'nothing_4784 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybe'45'concatMap_4800 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'mapMaybe_4806 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → T__'8804'__22 Source #
du_length'45'mapMaybe_4806 ∷ (AgdaAny → Maybe AgdaAny) → [AgdaAny] → T__'8804'__22 Source #
d_mapMaybe'45''43''43'_4818 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybe'45'map_4838 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'mapMaybe_4854 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → Maybe AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybe'45'map'45'retract_4870 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybe'45'map'45'none_4890 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybeIsInj'8321''8728'mapInj'8321'_4898 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybeIsInj'8321''8728'mapInj'8322'_4904 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybeIsInj'8322''8728'mapInj'8322'_4910 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_mapMaybeIsInj'8322''8728'mapInj'8321'_4916 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_length'45'applyUpTo_4924 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_lookup'45'applyUpTo_4938 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T_Fin_10 → T__'8801'__12 Source #
d_applyUpTo'45''8759''691'_4954 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_map'45'applyUpTo_4970 ∷ T_Level_18 → () → T_Level_18 → () → (Integer → AgdaAny) → (AgdaAny → AgdaAny) → Integer → T__'8801'__12 Source #
d_length'45'applyDownFrom_4994 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_lookup'45'applyDownFrom_5002 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T_Fin_10 → T__'8801'__12 Source #
d_applyDownFrom'45''8759''691'_5012 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_map'45'applyDownFrom_5022 ∷ T_Level_18 → () → (Integer → AgdaAny) → T_Level_18 → () → (AgdaAny → AgdaAny) → Integer → T__'8801'__12 Source #
d_map'45'upTo_5050 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_map'45'downFrom_5070 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_tabulate'45'cong_5078 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → (T_Fin_10 → T__'8801'__12) → T__'8801'__12 Source #
d_tabulate'45'lookup_5088 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_length'45'tabulate_5100 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → T__'8801'__12 Source #
d_lookup'45'tabulate_5118 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → T_Fin_10 → T__'8801'__12 Source #
d_map'45'tabulate_5132 ∷ T_Level_18 → () → T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_length'45''37''61'_5152 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_length'45''8759''61'_5174 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → AgdaAny → T__'8801'__12 Source #
d_map'45''8759''61'_5192 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T_Fin_10 → AgdaAny → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_length'45'insertAt_5220 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → AgdaAny → T__'8801'__12 Source #
d_length'45'removeAt_5238 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → T__'8801'__12 Source #
d_length'45'removeAt'8242'_5254 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → T__'8801'__12 Source #
d_map'45'removeAt_5272 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T_Fin_10 → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_removeAt'45'insertAt_5296 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → AgdaAny → T__'8801'__12 Source #
d_insertAt'45'removeAt_5316 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → T__'8801'__12 Source #
d_length'45'take_5334 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8801'__12 Source #
d_take'45'map_5352 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Integer → [AgdaAny] → T__'8801'__12 Source #
d_take'45'suc_5372 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → T__'8801'__12 Source #
d_take'45'suc'45'tabulate_5394 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → T_Fin_10 → T__'8801'__12 Source #
d_take'45'all_5412 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8804'__22 → T__'8801'__12 Source #
d_take'45''91''93'_5426 ∷ T_Level_18 → () → Integer → T__'8801'__12 Source #
d_take'45'take_5436 ∷ T_Level_18 → () → Integer → Integer → [AgdaAny] → T__'8801'__12 Source #
d_take'45'drop_5466 ∷ T_Level_18 → () → Integer → Integer → [AgdaAny] → T__'8801'__12 Source #
d_length'45'drop_5488 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8801'__12 Source #
d_drop'45'map_5506 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Integer → [AgdaAny] → T__'8801'__12 Source #
d_drop'45''91''93'_5520 ∷ T_Level_18 → () → Integer → T__'8801'__12 Source #
d_take'43''43'drop'8801'id_5528 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8801'__12 Source #
d_drop'45'take'45'suc_5548 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → T__'8801'__12 Source #
d_drop'45'take'45'suc'45'tabulate_5568 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → T_Fin_10 → T__'8801'__12 Source #
d_drop'45'drop_5588 ∷ T_Level_18 → () → Integer → Integer → [AgdaAny] → T__'8801'__12 Source #
d_drop'45'all_5610 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8804'__22 → T__'8801'__12 Source #
d_length'45'replicate_5626 ∷ T_Level_18 → () → Integer → AgdaAny → T__'8801'__12 Source #
d_lookup'45'replicate_5636 ∷ T_Level_18 → () → Integer → AgdaAny → T_Fin_10 → T__'8801'__12 Source #
d_map'45'replicate_5654 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Integer → AgdaAny → T__'8801'__12 Source #
d_zipWith'45'replicate_5676 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → Integer → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8801'__12 Source #
d_length'45'iterate_5700 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → Integer → T__'8801'__12 Source #
d_iterate'45'id_5716 ∷ T_Level_18 → () → AgdaAny → Integer → T__'8801'__12 Source #
d_lookup'45'iterate_5734 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → Integer → T_Fin_10 → T__'8801'__12 Source #
d_splitAt'45'defn_5752 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8801'__12 Source #
d_splitAt'45'map_5778 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Integer → [AgdaAny] → T__'8801'__12 Source #
d_takeWhile'43''43'dropWhile_5806 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8801'__12 Source #
d_span'45'defn_5826 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'filter_5860 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8804'__22 Source #
du_length'45'filter_5860 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8804'__22 Source #
d_filter'45'all_5886 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_filter'45'notAll_5922 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T__'8804'__22 Source #
du_filter'45'notAll_5922 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T__'8804'__22 Source #
d_filter'45'some_5978 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T__'8804'__22 Source #
du_filter'45'some_5978 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T__'8804'__22 Source #
d_filter'45'none_6028 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_filter'45'complete_6062 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_filter'45'accept_6094 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → AgdaAny → T__'8801'__12 Source #
d_filter'45'reject_6118 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → (AgdaAny → T_Irrelevant_20) → T__'8801'__12 Source #
d_filter'45'idem_6138 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8801'__12 Source #
d_filter'45''43''43'_6168 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_filter'45''8784'_6220 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → T_Dec_20) → T_Σ_14 → [AgdaAny] → T__'8801'__12 Source #
d_length'45'derun_6266 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T__'8804'__22 Source #
du_length'45'derun_6266 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T__'8804'__22 Source #
d_length'45'deduplicate_6300 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T__'8804'__22 Source #
du_length'45'deduplicate_6300 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T__'8804'__22 Source #
d_r_6310 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → [AgdaAny] Source #
d_derun'45'reject_6318 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → [AgdaAny] → AgdaAny → T__'8801'__12 Source #
d_derun'45'accept_6356 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → [AgdaAny] → (AgdaAny → T_Irrelevant_20) → T__'8801'__12 Source #
d_partition'45'defn_6400 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8801'__12 Source #
d_length'45'partition_6434 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Σ_14 Source #
d_partition'45'is'45'foldr_6464 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8801'__12 Source #
d_'691''43''43''45'defn_6496 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_'43''43''45''691''43''43'_6512 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_'691''43''43''45''691''43''43'_6528 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_length'45''691''43''43'_6542 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_map'45''691''43''43'_6556 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_foldr'45''691''43''43'_6576 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_foldl'45''691''43''43'_6600 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_unfold'45'reverse_6620 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45''43''43'_6630 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'selfInverse_6636 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_reverse'45'involutive_6646 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'injective_6648 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_length'45'reverse_6652 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'map_6658 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'foldr_6668 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'foldl_6682 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'applyUpTo_6694 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_reverse'45'applyDownFrom_6712 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → T__'8801'__12 Source #
d_'8759''691''45'injective_6730 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Σ_14 Source #
d_'8759''691''45'injective'737'_6754 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'8759''691''45'injective'691'_6766 ∷ T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T__'8801'__12 Source #
d_'8759''691''45''43''43'_6780 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_uncons'45'map_6798 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_head'45'map_6814 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_last'45'map_6826 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_tail'45'map_6844 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45'id'8322'_6850 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_map'45'cong'8322'_6852 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_map'45'compose_6854 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_map'45''43''43''45'commute_6856 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45'map'45'commute_6858 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_reverse'45''43''43''45'commute_6860 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'identity'737'_6862 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_zipWith'45'identity'691'_6864 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_'691''43''43''45''43''43'_6866 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T__'8801'__12 Source #
d_take'43''43'drop_6868 ∷ T_Level_18 → () → Integer → [AgdaAny] → T__'8801'__12 Source #
d_length'45''9472'_6870 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → T__'8801'__12 Source #
d_map'45''9472'_6872 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → T_Fin_10 → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_scanr'45'defn_6878 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_scanl'45'defn_6918 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T__'8801'__12 Source #
d_concat'45''91''45''93'_6938 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_sum'45''43''43'_6944 ∷ [Integer] → [Integer] → T__'8801'__12 Source #