Documentation

d_Fin_10 ∷ p → () Source #

data T_Fin_10 Source #

d_toℕ_18 ∷ Integer → T_Fin_10 → Integer Source #

du_toℕ_18 ∷ T_Fin_10 → Integer Source #

d_Fin'8242'_22 ∷ Integer → T_Fin_10 → () Source #

d_cast_26 ∷ Integer → Integer → T__'8801'__12 → T_Fin_10 → T_Fin_10 Source #

du_cast_26 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d_fromℕ_48 ∷ Integer → T_Fin_10 Source #

d_fromℕ'60'_52 ∷ Integer → Integer → T__'8804'__22 → T_Fin_10 Source #

du_fromℕ'60'_52 ∷ Integer → T_Fin_10 Source #

d_fromℕ'60''8243'_62 ∷ Integer → Integer → T__'8739''737'__28 → T_Fin_10 Source #

du_fromℕ'60''8243'_62 ∷ Integer → T_Fin_10 Source #

d__'8593''737'__72 ∷ Integer → T_Fin_10 → Integer → T_Fin_10 Source #

du__'8593''737'__72 ∷ T_Fin_10 → T_Fin_10 Source #

d__'8593''691'__84 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 Source #

du__'8593''691'__84 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d_reduce'8805'_94 ∷ Integer → Integer → T_Fin_10 → T__'8804'__22 → T_Fin_10 Source #

du_reduce'8805'_94 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d_inject_104 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du_inject_104 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_inject'33'_114 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du_inject'33'_114 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_inject'8321'_118 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

du_inject'8321'_118 ∷ T_Fin_10 → T_Fin_10 Source #

d_inject'8804'_122 ∷ Integer → Integer → T_Fin_10 → T__'8804'__22 → T_Fin_10 Source #

du_inject'8804'_122 ∷ T_Fin_10 → T_Fin_10 Source #

d_lower'8321'_130 ∷ Integer → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T_Fin_10 Source #

du_lower'8321'_130 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d_lower_144 ∷ Integer → Integer → T_Fin_10 → T__'8804'__22 → T_Fin_10 Source #

du_lower_144 ∷ T_Fin_10 → T_Fin_10 Source #

d_strengthen_158 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

du_strengthen_158 ∷ T_Fin_10 → T_Fin_10 Source #

d_splitAt_166 ∷ Integer → Integer → T_Fin_10 → T__'8846'__30 Source #

du_splitAt_166 ∷ Integer → T_Fin_10 → T__'8846'__30 Source #

d_join_180 ∷ Integer → Integer → T__'8846'__30 → T_Fin_10 Source #

du_join_180 ∷ Integer → T__'8846'__30 → T_Fin_10 Source #

d_quotRem_192 ∷ Integer → Integer → T_Fin_10 → T_Σ_14 Source #

du_quotRem_192 ∷ Integer → T_Fin_10 → T_Σ_14 Source #

d_remQuot_204 ∷ Integer → Integer → T_Fin_10 → T_Σ_14 Source #

du_remQuot_204 ∷ Integer → T_Fin_10 → T_Σ_14 Source #

d_quotient_210 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 Source #

du_quotient_210 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d_remainder_216 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 Source #

du_remainder_216 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d_combine_222 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du_combine_222 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_finToFun_238 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_funToFin_254 ∷ Integer → Integer → (T_Fin_10 → T_Fin_10) → T_Fin_10 Source #

d_fold_272 ∷ T_Level_18 → (Integer → ()) → Integer → (Integer → AgdaAny → AgdaAny) → (Integer → AgdaAny) → T_Fin_10 → AgdaAny Source #

du_fold_272 ∷ Integer → (Integer → AgdaAny → AgdaAny) → (Integer → AgdaAny) → T_Fin_10 → AgdaAny Source #

d_fold'8242'_298 ∷ Integer → T_Level_18 → (T_Fin_10 → ()) → (T_Fin_10 → AgdaAny → AgdaAny) → AgdaAny → T_Fin_10 → AgdaAny Source #

du_fold'8242'_298 ∷ (T_Fin_10 → AgdaAny → AgdaAny) → AgdaAny → T_Fin_10 → AgdaAny Source #

d_lift_318 ∷ Integer → Integer → Integer → (T_Fin_10 → T_Fin_10) → T_Fin_10 → T_Fin_10 Source #

du_lift_318 ∷ Integer → (T_Fin_10 → T_Fin_10) → T_Fin_10 → T_Fin_10 Source #

d__'43'__338 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du__'43'__338 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d__'45'__350 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du__'45'__350 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d__ℕ'45'__362 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d__ℕ'45'ℕ__372 ∷ Integer → T_Fin_10 → Integer Source #

d_pred_380 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

du_pred_380 ∷ T_Fin_10 → T_Fin_10 Source #

d_opposite_384 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d_punchOut_396 ∷ Integer → T_Fin_10 → T_Fin_10 → (T__'8801'__12 → T_Irrelevant_20) → T_Fin_10 Source #

du_punchOut_396 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_punchIn_410 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du_punchIn_410 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_pinch_420 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du_pinch_420 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d__'8804'__434 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → () Source #

d__'8805'__440 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → () Source #

d__'60'__446 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → () Source #

d__'62'__452 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → () Source #

d__'8816'__460 ∷ Integer → T_Fin_10 → T_Fin_10 → () Source #

d__'8814'__468 ∷ Integer → T_Fin_10 → T_Fin_10 → () Source #

d_Ordering_476 ∷ p → p → p → () Source #

data T_Ordering_476 Source #

d_compare_500 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Ordering_476 Source #

du_compare_500 ∷ T_Fin_10 → T_Fin_10 → T_Ordering_476 Source #

d_raise_536 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 Source #

d_inject'43'_542 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 Source #

du_inject'43'_542 ∷ T_Fin_10 → T_Fin_10 Source #

d__'8826'__548 ∷ p → p → () Source #

newtype T__'8826'__548 Source #