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'__26 → 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_strengthen_144 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

du_strengthen_144 ∷ T_Fin_10 → T_Fin_10 Source #

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

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

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

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

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

du_quotRem_178 ∷ Integer → T_Fin_10 → T_Σ_14 Source #

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

du_remQuot_190 ∷ Integer → T_Fin_10 → T_Σ_14 Source #

d_quotient_196 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 Source #

du_quotient_196 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d_remainder_202 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 Source #

du_remainder_202 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

d_combine_208 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du_combine_208 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_finToFun_224 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

d_pred_366 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

du_pred_366 ∷ T_Fin_10 → T_Fin_10 Source #

d_opposite_370 ∷ Integer → T_Fin_10 → T_Fin_10 Source #

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

du_punchOut_382 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_punchIn_396 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du_punchIn_396 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

d_pinch_406 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

du_pinch_406 ∷ T_Fin_10 → T_Fin_10 → T_Fin_10 Source #

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

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

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

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

d_Ordering_446 ∷ p → p → p → () Source #

data T_Ordering_446 Source #

d_compare_470 ∷ Integer → T_Fin_10 → T_Fin_10 → T_Ordering_446 Source #

du_compare_470 ∷ T_Fin_10 → T_Fin_10 → T_Ordering_446 Source #

d_raise_506 ∷ Integer → Integer → T_Fin_10 → T_Fin_10 Source #

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

du_inject'43'_512 ∷ T_Fin_10 → T_Fin_10 Source #

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

newtype T__'8826'__518 Source #