Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Documentation
d_isEquivalence_56 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsEquivalence_26 Source #
d_isDecEquivalence_76 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #
d_isPreorder_100 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPreorder_70 Source #
d_isPartialOrder_136 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #
d_All'45'resp'45'Pointwise_194 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #
du_All'45'resp'45'Pointwise_194 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #
d_Any'45'resp'45'Pointwise_210 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #
du_Any'45'resp'45'Pointwise_210 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #
d_AllPairs'45'resp'45'Pointwise_228 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #
du_AllPairs'45'resp'45'Pointwise_228 ∷ T_Σ_14 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #
d_Pointwise'45'length_244 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T__'8801'__12 Source #
d_tabulate'8314'_258 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → Integer → (T_Fin_6 → AgdaAny) → (T_Fin_6 → AgdaAny) → (T_Fin_6 → AgdaAny) → T_Pointwise_48 Source #
du_tabulate'8314'_258 ∷ Integer → (T_Fin_6 → AgdaAny) → T_Pointwise_48 Source #
d_tabulate'8315'_274 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → Integer → (T_Fin_6 → AgdaAny) → (T_Fin_6 → AgdaAny) → T_Pointwise_48 → T_Fin_6 → AgdaAny Source #
d_'43''43''8314'_290 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_'43''43''8314'_290 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_'43''43''45'cancel'737'_302 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_'43''43''45'cancel'691'_316 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_concat'8314'_350 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [[AgdaAny]] → [[AgdaAny]] → T_Pointwise_48 → T_Pointwise_48 Source #
du_concat'8314'_350 ∷ [[AgdaAny]] → [[AgdaAny]] → T_Pointwise_48 → T_Pointwise_48 Source #
d_reverseAcc'8314'_356 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_reverseAcc'8314'_356 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_'691''43''43''8314'_366 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_'691''43''43''8314'_366 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_reverse'8314'_372 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_reverse'8314'_372 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_map'8314'_382 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Pointwise_48 → T_Pointwise_48 Source #
du_map'8314'_382 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_map'8315'_404 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Pointwise_48 → T_Pointwise_48 Source #
du_map'8315'_404 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_foldr'8314'_434 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_48 → AgdaAny Source #
du_foldr'8314'_434 ∷ [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_48 → AgdaAny Source #
d_filter'8314'_480 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → (AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_filter'8314'_480 ∷ (AgdaAny → T_Dec_32) → (AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_replicate'8314'_536 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → Integer → T_Pointwise_48 Source #
d_lookup'8315'_548 ∷ T_Level_18 → () → [AgdaAny] → T_Level_18 → () → [AgdaAny] → T_Level_18 → (AgdaAny → AgdaAny → ()) → T__'8801'__12 → (T_Fin_6 → T_Fin_6 → T__'8801'__12 → AgdaAny) → T_Pointwise_48 Source #
du_lookup'8315'_548 ∷ [AgdaAny] → [AgdaAny] → (T_Fin_6 → T_Fin_6 → T__'8801'__12 → AgdaAny) → T_Pointwise_48 Source #
d_lookup'8314'_560 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Fin_6 → AgdaAny Source #
du_lookup'8314'_560 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Fin_6 → AgdaAny Source #
d_Pointwise'45''8801''8658''8801'_568 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T__'8801'__12 Source #
d_'8801''8658'Pointwise'45''8801'_578 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Pointwise_48 Source #
d_Rel_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d_Rel'8801''8658''8801'_588 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T__'8801'__12 Source #
d_'8801''8658'Rel'8801'_590 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Pointwise_48 Source #
d_Rel'8596''8801'_592 ∷ T_Level_18 → () → T_Inverse_58 Source #
d_decidable'45''8801'_594 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → T_Dec_32 Source #