| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Relation.Unary.All.Properties
Documentation
d_Null'8658'null_50 ∷ T_Level_18 → () → [AgdaAny] → T_All_44 → AgdaAny Source #
d_null'8658'Null_52 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → T_All_44 Source #
d_'91''93''61''45'injective_62 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → AgdaAny → T_All_44 → T_Any_34 → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 → T__'8801'__12 Source #
d_'172'Any'8658'All'172'_70 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (T_Any_34 → T_'8869'_4) → T_All_44 Source #
du_'172'Any'8658'All'172'_70 ∷ [AgdaAny] → (T_Any_34 → T_'8869'_4) → T_All_44 Source #
d_All'172''8658''172'Any_82 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_Any_34 → T_'8869'_4 Source #
d_'172'All'8658'Any'172'_94 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → (T_All_44 → T_'8869'_4) → T_Any_34 Source #
d_Any'172''8658''172'All_134 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_All_44 → T_'8869'_4 Source #
d_'172'Any'8608'All'172'_142 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Surjection_54 Source #
d_to'8728'from_152 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_Any'172''8660''172'All_186 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_32) → T_Equivalence_16 Source #
d_All'45'swap_226 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #
d_'91''93''61'lookup_248 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → T__'91'_'93''61'__74 Source #
d_'91''93''61''8658'lookup_266 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → T__'91'_'93''61'__74 → T__'8801'__12 Source #
d_lookup'8658''91''93''61'_276 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → T__'8801'__12 → T__'91'_'93''61'__74 Source #
d_map'45'id_284 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_map'45'cong_300 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_All_44 → (AgdaAny → AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_map'45'compose_314 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 Source #
d_lookup'45'map_328 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T_All_44 → T_Any_34 → T__'8801'__12 Source #
d_updateAt'45'updates_348 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → AgdaAny → T_All_44 → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #
du_updateAt'45'updates_348 ∷ [AgdaAny] → T_Any_34 → T_All_44 → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #
d_updateAt'45'minimal_372 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_Any_34 → (AgdaAny → AgdaAny) → AgdaAny → T_All_44 → (T__'8801'__12 → T__'8801'__12 → T_'8869'_4) → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #
du_updateAt'45'minimal_372 ∷ [AgdaAny] → T_Any_34 → T_Any_34 → T_All_44 → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #
d_lookup'8728'updateAt_416 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_lookup'8728'updateAt'8242'_432 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_Any_34 → (AgdaAny → AgdaAny) → AgdaAny → T_All_44 → (T__'8801'__12 → T__'8801'__12 → T_'8869'_4) → T__'8801'__12 Source #
d_updateAt'45'id'45'relative_448 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 → T__'8801'__12 Source #
d_updateAt'45'id_472 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_All_44 → T__'8801'__12 Source #
d_updateAt'45'compose'45'relative_488 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 → T__'8801'__12 Source #
d_updateAt'45'compose_514 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 Source #
d_updateAt'45'cong'45'relative_536 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T__'8801'__12 → T__'8801'__12 Source #
d_updateAt'45'cong_562 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T_All_44 → T__'8801'__12 Source #
d_updateAt'45'commutes_578 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → AgdaAny → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_Any_34 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (T__'8801'__12 → T__'8801'__12 → T_'8869'_4) → T_All_44 → T__'8801'__12 Source #
d_map'45'updateAt_624 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_All_44 → T_Any_34 → T__'8801'__12 → T__'8801'__12 Source #
d_singleton'8315'_642 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_All_44 → AgdaAny Source #
d_head'8314'_646 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_tail'8314'_650 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_last'8314'_654 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_uncons'8314'_662 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_uncons'8315'_668 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_18 → T_All_44 Source #
d_map'8314'_680 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #
d_map'8315'_688 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #
d_gmap_696 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_mapMaybe'8314'_702 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → Maybe AgdaAny) → T_All_44 → T_All_44 Source #
d_'43''43''8314'_760 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 → T_All_44 Source #
d_'43''43''8315''737'_774 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #
d_'43''43''8315''691'_790 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #
d_'43''43''8315'_806 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_Σ_14 Source #
d_'43''43''8596'_820 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Inverse_58 Source #
d_'43''43''8314''8728''43''43''8315'_832 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_'43''43''8315''8728''43''43''8314'_846 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Σ_14 → T__'8801'__12 Source #
d_concat'8314'_862 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [[AgdaAny]] → T_All_44 → T_All_44 Source #
d_concat'8315'_870 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [[AgdaAny]] → T_All_44 → T_All_44 Source #
d_'8759''691''8314'_878 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny → T_All_44 Source #
d_'8759''691''8315'_884 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Σ_14 Source #
d_unsnoc'8314'_888 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_unsnoc'8315'_906 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_18 → T_All_44 Source #
d__'8712'__942 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → AgdaAny → [AgdaAny] → () Source #
d__'8712'__946 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → AgdaAny → [AgdaAny] → () Source #
d_cartesianProductWith'8314'_958 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #
du_cartesianProductWith'8314'_958 ∷ T_Setoid_44 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #
d_cartesianProduct'8314'_984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Level_18 → (T_Σ_14 → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #
du_cartesianProduct'8314'_984 ∷ T_Setoid_44 → T_Setoid_44 → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #
d_drop'8314'_988 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → Integer → T_All_44 → T_All_44 Source #
d_dropWhile'8314'_1002 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_32) → T_All_44 → T_All_44 Source #
d_dropWhile'8315'_1042 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_32) → T__'8801'__12 → T_All_44 Source #
d_all'45'head'45'dropWhile_1084 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_All_18 Source #
d_take'8314'_1116 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → Integer → T_All_44 → T_All_44 Source #
d_takeWhile'8314'_1130 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_32) → T_All_44 → T_All_44 Source #
d_takeWhile'8315'_1170 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_32) → T__'8801'__12 → T_All_44 Source #
d_all'45'takeWhile_1212 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_All_44 Source #
d_applyUpTo'8314''8321'_1248 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → T__'8804'__18 → AgdaAny) → T_All_44 Source #
d_applyUpTo'8314''8322'_1266 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → AgdaAny) → T_All_44 Source #
d_applyUpTo'8315'_1282 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → T_All_44 → Integer → T__'8804'__18 → AgdaAny Source #
d_applyDownFrom'8314''8321'_1312 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → T__'8804'__18 → AgdaAny) → T_All_44 Source #
du_applyDownFrom'8314''8321'_1312 ∷ Integer → (Integer → T__'8804'__18 → AgdaAny) → T_All_44 Source #
d_applyDownFrom'8314''8322'_1330 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → AgdaAny) → T_All_44 Source #
d_tabulate'8314'_1346 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Integer → (T_Fin_6 → AgdaAny) → (T_Fin_6 → AgdaAny) → T_All_44 Source #
d_tabulate'8315'_1360 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Integer → (T_Fin_6 → AgdaAny) → T_All_44 → T_Fin_6 → AgdaAny Source #
d_'9472''8314'_1374 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_All_44 → T_All_44 Source #
d_'9472''8315'_1388 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → AgdaAny → T_All_44 → T_All_44 Source #
d_all'45'filter_1414 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_All_44 Source #
d_filter'8314'_1434 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_filter'8315'_1458 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 → T_All_44 Source #
d_partition'45'All_1540 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_Σ_14 Source #
d_derun'8314'_1560 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_deduplicate'8314'_1600 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
du_deduplicate'8314'_1600 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_derun'8315'_1608 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #
du_derun'8315'_1608 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_aux_1632 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 → AgdaAny → [AgdaAny] → T_All_44 → T_All_44 Source #
du_aux_1632 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 → T_All_44 Source #
d_deduplicate'8315'_1690 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #
du_deduplicate'8315'_1690 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_aux_1714 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny → T_Any_34 → AgdaAny Source #
du_aux_1714 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_zipWith'8314'_1726 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → T_Pointwise_48 → T_All_44 Source #
du_zipWith'8314'_1726 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 Source #
d_fromMaybe'8314'_1738 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Maybe AgdaAny → T_All_18 → T_All_44 Source #
d_fromMaybe'8315'_1744 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Maybe AgdaAny → T_All_44 → T_All_18 Source #
d_replicate'8314'_1754 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → Integer → AgdaAny → T_All_44 Source #
d_replicate'8315'_1764 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → Integer → T_All_44 → AgdaAny Source #
d_inits'8314'_1768 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_inits'8315'_1778 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_tails'8314'_1794 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_tails'8315'_1802 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_all'8314'_1822 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → AgdaAny → T_All_44 Source #
d_all'8315'_1844 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_All_44 → AgdaAny Source #
d_anti'45'mono_1850 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Any_34 → T_Any_34) → T_All_44 → T_All_44 Source #
du_anti'45'mono_1850 ∷ [AgdaAny] → [AgdaAny] → (AgdaAny → T_Any_34 → T_Any_34) → T_All_44 → T_All_44 Source #
d_all'45'anti'45'mono_1858 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → (AgdaAny → Bool) → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → AgdaAny Source #
du_all'45'anti'45'mono_1858 ∷ [AgdaAny] → [AgdaAny] → (AgdaAny → Bool) → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → AgdaAny Source #
d__'8779'__1898 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → [AgdaAny] → [AgdaAny] → () Source #
d_respects_1906 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #
du_respects_1906 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #
d_All'45'all_1920 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_All_44 → AgdaAny Source #
d_all'45'All_1922 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → AgdaAny → T_All_44 Source #
d_All'45'map_1924 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #
d_map'45'All_1926 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #
d_filter'8314''8321'_1928 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → [AgdaAny] → T_All_44 Source #
d_filter'8314''8322'_1930 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_Any'172''8594''172'All_1932 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_All_44 → T_'8869'_4 Source #