| 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_'91''93''61'lookup_72 ∷ 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_90 ∷ 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'_100 ∷ 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'cong_114 ∷ 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'id_124 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T__'8801'__12 Source #
d_map'45''8728'_138 ∷ 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_152 ∷ 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_172 ∷ 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_172 ∷ [AgdaAny] → T_Any_34 → T_All_44 → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #
d_updateAt'45'minimal_196 ∷ 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_Irrelevant_20) → T__'91'_'93''61'__74 → T__'91'_'93''61'__74 Source #
du_updateAt'45'minimal_196 ∷ [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_240 ∷ 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'_256 ∷ 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_Irrelevant_20) → T__'8801'__12 Source #
d_updateAt'45'id'45'local_272 ∷ 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_296 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → T_All_44 → T__'8801'__12 Source #
d_updateAt'45''8728''45'local_312 ∷ 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''8728'_338 ∷ 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'local_352 ∷ 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_378 ∷ 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_394 ∷ 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_Irrelevant_20) → T_All_44 → T__'8801'__12 Source #
d_map'45'updateAt_440 ∷ 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'_458 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → T_All_44 → AgdaAny Source #
d_head'8314'_462 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_tail'8314'_466 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_last'8314'_470 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_uncons'8314'_478 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_uncons'8315'_484 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_18 → T_All_44 Source #
d_map'8314'_496 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #
d_map'8315'_504 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #
d_gmap'8314'_512 ∷ 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_gmap'8315'_518 ∷ 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'_524 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → Maybe AgdaAny) → T_All_44 → T_All_44 Source #
d_All'45'catMaybes'8314'_570 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [Maybe AgdaAny] → T_All_44 → T_All_44 Source #
d_Any'45'catMaybes'8314'_578 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [Maybe AgdaAny] → T_All_44 → T_All_44 Source #
d_'43''43''8314'_580 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 → T_All_44 Source #
d_'43''43''8315''737'_594 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #
d_'43''43''8315''691'_610 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #
d_'43''43''8315'_626 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_All_44 → T_Σ_14 Source #
d_'43''43''8596'_640 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #
d_'43''43''8314''8728''43''43''8315'_652 ∷ 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'_666 ∷ 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'_682 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [[AgdaAny]] → T_All_44 → T_All_44 Source #
d_concat'8315'_690 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [[AgdaAny]] → T_All_44 → T_All_44 Source #
d_'8759''691''8314'_698 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny → T_All_44 Source #
d_'8759''691''8315'_704 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Σ_14 Source #
d_unsnoc'8314'_708 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_18 Source #
d_unsnoc'8315'_726 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_18 → T_All_44 Source #
d__'8712'__762 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8712'__766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_cartesianProductWith'8314'_778 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → 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'_778 ∷ T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #
d_cartesianProduct'8314'_804 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Level_18 → (T_Σ_14 → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #
du_cartesianProduct'8314'_804 ∷ T_Setoid_46 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_All_44 Source #
d_drop'8314'_808 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → Integer → T_All_44 → T_All_44 Source #
d_dropWhile'8314'_822 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 → T_All_44 Source #
d_dropWhile'8315'_862 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T__'8801'__12 → T_All_44 Source #
d_all'45'head'45'dropWhile_904 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_18 Source #
d_all'8658'dropWhile'8801''91''93'_936 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 → T__'8801'__12 Source #
d_take'8314'_952 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → Integer → T_All_44 → T_All_44 Source #
d_takeWhile'8314'_966 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 → T_All_44 Source #
d_all'45'takeWhile_1008 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 Source #
d_all'8658'takeWhile'8791'id_1040 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T_All_44 → T__'8801'__12 Source #
d_applyUpTo'8314''8321'_1062 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → T__'8804'__22 → AgdaAny) → T_All_44 Source #
d_applyUpTo'8314''8322'_1080 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → AgdaAny) → T_All_44 Source #
d_applyUpTo'8315'_1096 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → T_All_44 → Integer → T__'8804'__22 → AgdaAny Source #
d_applyDownFrom'8314''8321'_1126 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → T__'8804'__22 → AgdaAny) → T_All_44 Source #
du_applyDownFrom'8314''8321'_1126 ∷ Integer → (Integer → T__'8804'__22 → AgdaAny) → T_All_44 Source #
d_applyDownFrom'8314''8322'_1144 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (Integer → AgdaAny) → Integer → (Integer → AgdaAny) → T_All_44 Source #
d_tabulate'8314'_1160 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → T_All_44 Source #
d_tabulate'8315'_1172 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Integer → (T_Fin_10 → AgdaAny) → T_All_44 → T_Fin_10 → AgdaAny Source #
d_'9472''8314'_1182 ∷ 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'_1196 ∷ 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_1222 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 Source #
d_filter'8314'_1242 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_filter'8315'_1266 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 → T_All_44 Source #
d_partition'45'All_1338 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Σ_14 Source #
d_derun'8314'_1358 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_deduplicate'8314'_1398 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
du_deduplicate'8314'_1398 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_derun'8315'_1406 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #
du_derun'8315'_1406 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_aux_1430 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → 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_1430 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_All_44 → T_All_44 Source #
d_deduplicate'8315'_1478 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #
du_deduplicate'8315'_1478 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_aux_1502 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → AgdaAny → T_All_44 → AgdaAny → T_Any_34 → AgdaAny Source #
du_aux_1502 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_zipWith'8314'_1514 ∷ 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'_1514 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 Source #
d_fromMaybe'8314'_1526 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Maybe AgdaAny → T_All_18 → T_All_44 Source #
d_fromMaybe'8315'_1532 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → Maybe AgdaAny → T_All_44 → T_All_18 Source #
d_replicate'8314'_1542 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → Integer → AgdaAny → T_All_44 Source #
d_replicate'8315'_1552 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → Integer → T_All_44 → AgdaAny Source #
d_inits'8314'_1556 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_inits'8315'_1566 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_tails'8314'_1582 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_tails'8315'_1590 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_All_44 Source #
d_all'8314'_1610 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → AgdaAny → T_All_44 Source #
d_all'8315'_1622 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → T_All_44 → AgdaAny Source #
d_anti'45'mono_1628 ∷ 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_1628 ∷ [AgdaAny] → [AgdaAny] → (AgdaAny → T_Any_34 → T_Any_34) → T_All_44 → T_All_44 Source #
d_all'45'anti'45'mono_1636 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → (AgdaAny → Bool) → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → AgdaAny Source #
du_all'45'anti'45'mono_1636 ∷ [AgdaAny] → [AgdaAny] → (AgdaAny → Bool) → (AgdaAny → T_Any_34 → T_Any_34) → AgdaAny → AgdaAny Source #
d__'8779'__1678 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → () Source #
d_respects_1736 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #
du_respects_1736 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #
d_Any'172''8594''172'All_1750 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_All_44 → T_Irrelevant_20 Source #
d_updateAt'45'id'45'relative_1752 ∷ 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'compose'45'relative_1754 ∷ 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_1756 ∷ 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_1758 ∷ 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_gmap_1760 ∷ 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_map'45'compose_1762 ∷ 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_takeWhile'8315'_1766 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Dec_20) → T__'8801'__12 → T_All_44 Source #