| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Relation.Unary.All
Documentation
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 #
d_head_114 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → T_All_44 → AgdaAny Source #
d_tail_116 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → 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 #
d_construct_136 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (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 #
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 #
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 #
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 #
d_zip_198 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [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 #
d__'8712'__240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → () Source #
d_tabulate'8347'_256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_All_44 Source #
du_tabulate'8347'_256 ∷ T_Setoid_44 → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_All_44 Source #
d_tabulate_264 ∷ T_Level_18 → () → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Any_34 → AgdaAny) → T_All_44 Source #
d_self_268 ∷ T_Level_18 → () → [AgdaAny] → T_All_44 Source #
du_self_268 ∷ [AgdaAny] → T_All_44 Source #
d_updateAt_274 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Any_34 → (AgdaAny → AgdaAny) → T_All_44 → T_All_44 Source #
d__'91'_'93''37''61'__292 ∷ 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'__292 ∷ [AgdaAny] → T_All_44 → T_Any_34 → (AgdaAny → AgdaAny) → T_All_44 Source #
d__'91'_'93''8788'__300 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → AgdaAny → T_All_44 → T_Any_34 → AgdaAny → T_All_44 Source #
d_sequenceA_358 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawApplicative_20 → [AgdaAny] → T_All_44 → AgdaAny Source #
du_sequenceA_358 ∷ T_RawApplicative_20 → [AgdaAny] → T_All_44 → AgdaAny Source #
d_mapA_366 ∷ 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_366 ∷ T_RawApplicative_20 → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → AgdaAny Source #
d_forA_372 ∷ 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_372 ∷ T_RawApplicative_20 → [AgdaAny] → T_All_44 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #
d_App_394 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawMonad_24 → T_RawApplicative_20 Source #
d_sequenceM_396 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawMonad_24 → [AgdaAny] → T_All_44 → AgdaAny Source #
du_sequenceM_396 ∷ T_RawMonad_24 → [AgdaAny] → T_All_44 → AgdaAny Source #
d_mapM_400 ∷ 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_400 ∷ T_RawMonad_24 → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 → AgdaAny Source #
d_forM_404 ∷ 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_404 ∷ T_RawMonad_24 → [AgdaAny] → T_All_44 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #
d_lookupAny_408 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_All_44 → T_Any_34 → T_Σ_14 Source #
d_lookupWith_424 ∷ 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_424 ∷ [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_All_44 → T_Any_34 → AgdaAny Source #
d_lookup_434 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → T_All_44 → AgdaAny → T_Any_34 → AgdaAny Source #
d_'46'extendedlambda0_438 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny] → T_All_44 → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d__'8776'__458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → ()) → AgdaAny → AgdaAny → () Source #
d__'8712'__480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → () Source #
d_lookup'8347'_496 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_All_44 → AgdaAny → T_Any_34 → AgdaAny Source #
du_lookup'8347'_496 ∷ T_Setoid_44 → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_All_44 → AgdaAny → T_Any_34 → AgdaAny Source #
d_all'63'_506 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Dec_20 Source #
d_universal_516 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → [AgdaAny] → T_All_44 Source #
d_universal'45'U_526 ∷ T_Level_18 → () → [AgdaAny] → T_All_44 Source #
d_irrelevant_528 ∷ 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_542 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Σ_14 Source #
d_decide_544 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T__'8846'__30) → [AgdaAny] → T__'8846'__30 Source #
du_decide_544 ∷ (AgdaAny → T__'8846'__30) → [AgdaAny] → T__'8846'__30 Source #
d_all_576 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Dec_20 Source #