Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Data.List.Relation.Unary.All

Documentation

d_All_44 ∷ p → p → p → p → p → () Source #

data T_All_44 Source #

Constructors

C_'91''93'_50
C__'8759'__60 AgdaAny T_All_44

d__'91'_'93''61'__74 ∷ p → p → p → p → p → p → p → p → p → () Source #

data T__'91'_'93''61'__74 Source #

Constructors

C_here_88
C_there_104 T__'91'_'93''61'__74

d_Null_106 ∷ T_Level_18 → () → [AgdaAny] → () Source #

d_uncons_108 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → T_All_44 → T_Σ_14 Source #

du_uncons_108 ∷ T_All_44 → T_Σ_14 Source #

d_head_114 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → T_All_44 → AgdaAny Source #

du_head_114 ∷ T_All_44 → AgdaAny Source #

d_tail_116 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → T_All_44 → T_All_44 Source #

du_tail_116 ∷ T_All_44 → T_All_44 Source #

d_reduce_122 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → T_All_44 → [AgdaAny] Source #

du_reduce_122 ∷ [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → T_All_44 → [AgdaAny] Source #

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

du_construct_136 ∷ (AgdaAny → T_Σ_14) → [AgdaAny] → T_Σ_14 Source #

d_fromList_148 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [T_Σ_14] → T_All_44 Source #

du_fromList_148 ∷ [T_Σ_14] → T_All_44 Source #

d_toList_156 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → [T_Σ_14] Source #

du_toList_156 ∷ [AgdaAny] → T_All_44 → [T_Σ_14] Source #

d_map_164 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

du_map_164 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → T_All_44 Source #

d_zipWith_174 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Σ_14 → AgdaAny) → [AgdaAny] → T_Σ_14 → T_All_44 Source #

du_zipWith_174 ∷ (AgdaAny → T_Σ_14 → AgdaAny) → [AgdaAny] → T_Σ_14 → T_All_44 Source #

d_unzipWith_188 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → T_Σ_14) → [AgdaAny] → T_All_44 → T_Σ_14 Source #

du_unzipWith_188 ∷ (AgdaAny → AgdaAny → T_Σ_14) → [AgdaAny] → T_All_44 → T_Σ_14 Source #

d_zip_198 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Σ_14 → T_All_44 Source #

du_zip_198 ∷ [AgdaAny] → T_Σ_14 → T_All_44 Source #

d_unzip_200 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_All_44 → T_Σ_14 Source #

du_unzip_200 ∷ [AgdaAny] → T_All_44 → T_Σ_14 Source #

d__'8712'__242 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → () Source #

d_tabulate'8347'_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_All_44 Source #

du_tabulate'8347'_258 ∷ T_Setoid_46 → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_All_44 Source #

d_tabulate_266 ∷ T_Level_18 → () → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Any_34 → AgdaAny) → T_All_44 Source #

du_tabulate_266 ∷ [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_All_44 Source #

d_self_270 ∷ T_Level_18 → () → [AgdaAny] → T_All_44 Source #

du_self_270 ∷ [AgdaAny] → T_All_44 Source #

d_updateAt_276 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #

du_updateAt_276 ∷ [AgdaAny] → T_Any_34 → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #

d__'91'_'93''37''61'__294 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → (AgdaAny → AgdaAny) → T_All_44 Source #

du__'91'_'93''37''61'__294 ∷ [AgdaAny] → T_All_44 → T_Any_34 → (AgdaAny → AgdaAny) → T_All_44 Source #

d__'91'_'93''8788'__302 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → AgdaAny → T_All_44 Source #

du__'91'_'93''8788'__302 ∷ [AgdaAny] → T_All_44 → T_Any_34 → AgdaAny → T_All_44 Source #

d_sequenceA_360 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawApplicative_20 → [AgdaAny] → T_All_44 → AgdaAny Source #

du_sequenceA_360 ∷ T_RawApplicative_20 → [AgdaAny] → T_All_44 → AgdaAny Source #

d_mapA_368 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawApplicative_20 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → AgdaAny Source #

du_mapA_368 ∷ T_RawApplicative_20 → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → AgdaAny Source #

d_forA_374 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawApplicative_20 → T_Level_18 → [AgdaAny] → (AgdaAny → ()) → T_All_44 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

du_forA_374 ∷ T_RawApplicative_20 → [AgdaAny] → T_All_44 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

d_App_396 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawMonad_24 → T_RawApplicative_20 Source #

du_App_396 ∷ T_RawMonad_24 → T_RawApplicative_20 Source #

d_sequenceM_398 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawMonad_24 → [AgdaAny] → T_All_44 → AgdaAny Source #

du_sequenceM_398 ∷ T_RawMonad_24 → [AgdaAny] → T_All_44 → AgdaAny Source #

d_mapM_402 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawMonad_24 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → AgdaAny Source #

du_mapM_402 ∷ T_RawMonad_24 → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → AgdaAny Source #

d_forM_406 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawMonad_24 → T_Level_18 → [AgdaAny] → (AgdaAny → ()) → T_All_44 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

du_forM_406 ∷ T_RawMonad_24 → [AgdaAny] → T_All_44 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

d_lookupAny_410 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_All_44 → T_Any_34 → T_Σ_14 Source #

du_lookupAny_410 ∷ [AgdaAny] → T_All_44 → T_Any_34 → T_Σ_14 Source #

d_lookupWith_426 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_All_44 → T_Any_34 → AgdaAny Source #

du_lookupWith_426 ∷ [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_All_44 → T_Any_34 → AgdaAny Source #

d_lookup_436 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → T_All_44 → AgdaAny → T_Any_34 → AgdaAny Source #

du_lookup_436 ∷ [AgdaAny] → T_All_44 → T_Any_34 → AgdaAny Source #

d_'46'extendedlambda0_440 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → T_All_44 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

du_'46'extendedlambda0_440 ∷ AgdaAny → AgdaAny Source #

d__'8776'__460 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → ()) → AgdaAny → AgdaAny → () Source #

d__'8712'__484 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → () Source #

d_lookup'8347'_500 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_All_44 → AgdaAny → T_Any_34 → AgdaAny Source #

du_lookup'8347'_500 ∷ T_Setoid_46 → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_All_44 → AgdaAny → T_Any_34 → AgdaAny Source #

d_all'63'_510 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Dec_20 Source #

du_all'63'_510 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Dec_20 Source #

d_universal_520 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 Source #

du_universal_520 ∷ (AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 Source #

d_universal'45'U_530 ∷ T_Level_18 → () → [AgdaAny] → T_All_44 Source #

du_universal'45'U_530 ∷ [AgdaAny] → T_All_44 Source #

d_irrelevant_532 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → [AgdaAny] → T_All_44 → T_All_44 → T__'8801'__12 Source #

d_satisfiable_546 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Σ_14 Source #

du_satisfiable_546 ∷ T_Σ_14 Source #

d_decide_548 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T__'8846'__30) → [AgdaAny] → T__'8846'__30 Source #

du_decide_548 ∷ (AgdaAny → T__'8846'__30) → [AgdaAny] → T__'8846'__30 Source #

d_search_582 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8846'__30 Source #

du_search_582 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T__'8846'__30 Source #

d_all_586 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Dec_20 Source #