Documentation

d_Fin_10 :: p -> () #

data T_Fin_10 #

d_toℕ_18 :: Integer -> T_Fin_10 -> Integer #

du_toℕ_18 :: T_Fin_10 -> Integer #

d_Fin'8242'_22 :: Integer -> T_Fin_10 -> () #

d_cast_26 :: Integer -> Integer -> T__'8801'__12 -> T_Fin_10 -> T_Fin_10 #

du_cast_26 :: Integer -> T_Fin_10 -> T_Fin_10 #

d_fromℕ_48 :: Integer -> T_Fin_10 #

d_fromℕ'60'_52 :: Integer -> Integer -> T__'8804'__22 -> T_Fin_10 #

du_fromℕ'60'_52 :: Integer -> T_Fin_10 #

d_fromℕ'60''8243'_62 :: Integer -> Integer -> T__'8739''737'__26 -> T_Fin_10 #

du_fromℕ'60''8243'_62 :: Integer -> T_Fin_10 #

d__'8593''737'__72 :: Integer -> T_Fin_10 -> Integer -> T_Fin_10 #

du__'8593''737'__72 :: T_Fin_10 -> T_Fin_10 #

d__'8593''691'__84 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 #

du__'8593''691'__84 :: Integer -> T_Fin_10 -> T_Fin_10 #

d_reduce'8805'_94 :: Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T_Fin_10 #

du_reduce'8805'_94 :: Integer -> T_Fin_10 -> T_Fin_10 #

d_inject_104 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

du_inject_104 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

d_inject'33'_114 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

du_inject'33'_114 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

d_inject'8321'_118 :: Integer -> T_Fin_10 -> T_Fin_10 #

du_inject'8321'_118 :: T_Fin_10 -> T_Fin_10 #

d_inject'8804'_122 :: Integer -> Integer -> T_Fin_10 -> T__'8804'__22 -> T_Fin_10 #

du_inject'8804'_122 :: T_Fin_10 -> T_Fin_10 #

d_lower'8321'_130 :: Integer -> T_Fin_10 -> (T__'8801'__12 -> T_Irrelevant_20) -> T_Fin_10 #

du_lower'8321'_130 :: Integer -> T_Fin_10 -> T_Fin_10 #

d_strengthen_144 :: Integer -> T_Fin_10 -> T_Fin_10 #

du_strengthen_144 :: T_Fin_10 -> T_Fin_10 #

d_splitAt_152 :: Integer -> Integer -> T_Fin_10 -> T__'8846'__30 #

du_splitAt_152 :: Integer -> T_Fin_10 -> T__'8846'__30 #

d_join_166 :: Integer -> Integer -> T__'8846'__30 -> T_Fin_10 #

du_join_166 :: Integer -> T__'8846'__30 -> T_Fin_10 #

d_quotRem_178 :: Integer -> Integer -> T_Fin_10 -> T_Σ_14 #

du_quotRem_178 :: Integer -> T_Fin_10 -> T_Σ_14 #

d_remQuot_190 :: Integer -> Integer -> T_Fin_10 -> T_Σ_14 #

du_remQuot_190 :: Integer -> T_Fin_10 -> T_Σ_14 #

d_quotient_196 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 #

du_quotient_196 :: Integer -> T_Fin_10 -> T_Fin_10 #

d_remainder_202 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 #

du_remainder_202 :: Integer -> T_Fin_10 -> T_Fin_10 #

d_combine_208 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

du_combine_208 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

d_finToFun_224 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

d_funToFin_240 :: Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 #

d_fold_258 :: T_Level_18 -> (Integer -> ()) -> Integer -> (Integer -> AgdaAny -> AgdaAny) -> (Integer -> AgdaAny) -> T_Fin_10 -> AgdaAny #

du_fold_258 :: Integer -> (Integer -> AgdaAny -> AgdaAny) -> (Integer -> AgdaAny) -> T_Fin_10 -> AgdaAny #

d_fold'8242'_284 :: Integer -> T_Level_18 -> (T_Fin_10 -> ()) -> (T_Fin_10 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_10 -> AgdaAny #

du_fold'8242'_284 :: (T_Fin_10 -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Fin_10 -> AgdaAny #

d_lift_304 :: Integer -> Integer -> Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10 #

du_lift_304 :: Integer -> (T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> T_Fin_10 #

d__'43'__324 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

du__'43'__324 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

d__'45'__336 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

du__'45'__336 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

d__ℕ'45'__348 :: Integer -> T_Fin_10 -> T_Fin_10 #

d__ℕ'45'ℕ__358 :: Integer -> T_Fin_10 -> Integer #

d_pred_366 :: Integer -> T_Fin_10 -> T_Fin_10 #

du_pred_366 :: T_Fin_10 -> T_Fin_10 #

d_opposite_370 :: Integer -> T_Fin_10 -> T_Fin_10 #

d_punchOut_382 :: Integer -> T_Fin_10 -> T_Fin_10 -> (T__'8801'__12 -> T_Irrelevant_20) -> T_Fin_10 #

du_punchOut_382 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

d_punchIn_396 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

du_punchIn_396 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

d_pinch_406 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

du_pinch_406 :: T_Fin_10 -> T_Fin_10 -> T_Fin_10 #

d__'8804'__420 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> () #

d__'8805'__426 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> () #

d__'60'__432 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> () #

d__'62'__438 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 -> () #

d_Ordering_446 :: p -> p -> p -> () #

data T_Ordering_446 #

d_compare_470 :: Integer -> T_Fin_10 -> T_Fin_10 -> T_Ordering_446 #

du_compare_470 :: T_Fin_10 -> T_Fin_10 -> T_Ordering_446 #

d_raise_506 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 #

d_inject'43'_512 :: Integer -> Integer -> T_Fin_10 -> T_Fin_10 #

du_inject'43'_512 :: T_Fin_10 -> T_Fin_10 #

d__'8826'__518 :: p -> p -> () #

newtype T__'8826'__518 #