Documentation

d_Fin_6 :: p -> () Source #

data T_Fin_6 Source #

d_toℕ_20 :: Integer -> T_Fin_6 -> Integer Source #

du_toℕ_20 :: T_Fin_6 -> Integer Source #

d_Fin'8242'_26 :: Integer -> T_Fin_6 -> () Source #

d_cast_36 :: Integer -> Integer -> T__'8801'__12 -> T_Fin_6 -> T_Fin_6 Source #

du_cast_36 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

d_fromℕ_58 :: Integer -> T_Fin_6 Source #

d_fromℕ'60'_66 :: Integer -> Integer -> T__'8804'__18 -> T_Fin_6 Source #

du_fromℕ'60'_66 :: Integer -> T_Fin_6 Source #

d_fromℕ'60''8243'_82 :: Integer -> Integer -> T__'8804''8243'__210 -> T_Fin_6 Source #

du_fromℕ'60''8243'_82 :: Integer -> T__'8804''8243'__210 -> T_Fin_6 Source #

d__'8593''737'__90 :: Integer -> T_Fin_6 -> Integer -> T_Fin_6 Source #

du__'8593''737'__90 :: T_Fin_6 -> T_Fin_6 Source #

d__'8593''691'__102 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 Source #

du__'8593''691'__102 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

d_reduce'8805'_118 :: Integer -> Integer -> T_Fin_6 -> T__'8804'__18 -> T_Fin_6 Source #

du_reduce'8805'_118 :: Integer -> T_Fin_6 -> T__'8804'__18 -> T_Fin_6 Source #

d_inject_134 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

du_inject_134 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d_inject'33'_146 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

du_inject'33'_146 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d_inject'8321'_152 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

du_inject'8321'_152 :: T_Fin_6 -> T_Fin_6 Source #

d_inject'8804'_160 :: Integer -> Integer -> T_Fin_6 -> T__'8804'__18 -> T_Fin_6 Source #

du_inject'8804'_160 :: T_Fin_6 -> T_Fin_6 Source #

d_lower'8321'_176 :: Integer -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T_Fin_6 Source #

du_lower'8321'_176 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

d_strengthen_194 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

du_strengthen_194 :: T_Fin_6 -> T_Fin_6 Source #

d_splitAt_202 :: Integer -> Integer -> T_Fin_6 -> T__'8846'__30 Source #

du_splitAt_202 :: Integer -> T_Fin_6 -> T__'8846'__30 Source #

d_join_216 :: Integer -> Integer -> T__'8846'__30 -> T_Fin_6 Source #

du_join_216 :: Integer -> T__'8846'__30 -> T_Fin_6 Source #

d_quotRem_230 :: Integer -> Integer -> T_Fin_6 -> T_Σ_14 Source #

du_quotRem_230 :: Integer -> T_Fin_6 -> T_Σ_14 Source #

d_remQuot_262 :: Integer -> Integer -> T_Fin_6 -> T_Σ_14 Source #

du_remQuot_262 :: Integer -> T_Fin_6 -> T_Σ_14 Source #

d_quotient_270 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 Source #

du_quotient_270 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

d_remainder_280 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 Source #

du_remainder_280 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

d_combine_290 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

du_combine_290 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d_finToFun_310 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d_funToFin_330 :: Integer -> Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 Source #

d_fold_348 :: T_Level_14 -> (Integer -> ()) -> Integer -> (Integer -> AgdaAny -> AgdaAny) -> (Integer -> AgdaAny) -> T_Fin_6 -> AgdaAny Source #

du_fold_348 :: Integer -> (Integer -> AgdaAny -> AgdaAny) -> (Integer -> AgdaAny) -> T_Fin_6 -> AgdaAny Source #

d_fold'8242'_374 :: Integer -> T_Level_14 -> (T_Fin_6 -> ()) -> (T_Fin_6 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_6 -> AgdaAny Source #

du_fold'8242'_374 :: (T_Fin_6 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_6 -> AgdaAny Source #

d_lift_398 :: Integer -> Integer -> Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6 Source #

du_lift_398 :: Integer -> (T_Fin_6 -> T_Fin_6) -> T_Fin_6 -> T_Fin_6 Source #

d__'43'__422 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

du__'43'__422 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d__'45'__436 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

du__'45'__436 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d__ℕ'45'__448 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

d__ℕ'45'ℕ__458 :: Integer -> T_Fin_6 -> Integer Source #

d_pred_468 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

du_pred_468 :: T_Fin_6 -> T_Fin_6 Source #

d_opposite_474 :: Integer -> T_Fin_6 -> T_Fin_6 Source #

d_punchOut_488 :: Integer -> T_Fin_6 -> T_Fin_6 -> (T__'8801'__12 -> T_'8869'_4) -> T_Fin_6 Source #

du_punchOut_488 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d_punchIn_508 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

du_punchIn_508 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d_pinch_520 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

du_pinch_520 :: T_Fin_6 -> T_Fin_6 -> T_Fin_6 Source #

d__'8804'__534 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> () Source #

d__'8805'__540 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> () Source #

d__'60'__546 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> () Source #

d__'62'__552 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 -> () Source #

d__'8826'__558 :: p1 -> p2 -> () Source #

newtype T__'8826'__558 Source #

d_Ordering_568 :: p1 -> p2 -> p3 -> () Source #

data T_Ordering_568 Source #

d_compare_594 :: Integer -> T_Fin_6 -> T_Fin_6 -> T_Ordering_568 Source #

du_compare_594 :: T_Fin_6 -> T_Fin_6 -> T_Ordering_568 Source #

d_fromℕ'8804'_630 :: Integer -> Integer -> T__'8804'__18 -> T_Fin_6 Source #

d_fromℕ'8804''8243'_632 :: Integer -> Integer -> T__'8804''8243'__210 -> T_Fin_6 Source #

d_raise_634 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 Source #

d_inject'43'_640 :: Integer -> Integer -> T_Fin_6 -> T_Fin_6 Source #

du_inject'43'_640 :: T_Fin_6 -> T_Fin_6 Source #