Documentation

d_Bwd_6 :: p -> () #

data T_Bwd_6 #

d_bwd'45'length_16 :: () -> T_Bwd_6 -> Integer #

du_bwd'45'length_16 :: T_Bwd_6 -> Integer #

d_bwd'45'foldr_26 :: () -> () -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Bwd_6 -> AgdaAny #

du_bwd'45'foldr_26 :: (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Bwd_6 -> AgdaAny #

d__'60''62''62'__42 :: () -> T_Bwd_6 -> [AgdaAny] -> [AgdaAny] #

du__'60''62''62'__42 :: T_Bwd_6 -> [AgdaAny] -> [AgdaAny] #

d__'60''62''60'__54 :: () -> T_Bwd_6 -> [AgdaAny] -> T_Bwd_6 #

du__'60''62''60'__54 :: T_Bwd_6 -> [AgdaAny] -> T_Bwd_6 #

d__'58''60'L__66 :: () -> [AgdaAny] -> AgdaAny -> [AgdaAny] #

du__'58''60'L__66 :: [AgdaAny] -> AgdaAny -> [AgdaAny] #

d__'8759'B__74 :: () -> AgdaAny -> T_Bwd_6 -> T_Bwd_6 #

du__'8759'B__74 :: AgdaAny -> T_Bwd_6 -> T_Bwd_6 #

d_lemma'60''62'1_90 :: () -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 #

d_lemma'60''62'1''_106 :: () -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 -> T__'8801'__12 #

d_lemma'60''62'2_118 :: () -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 #

d_lemma'60''62'2''_134 :: () -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 -> T__'8801'__12 #

d_lemma'45''60''62''62''45''43''43'_148 :: () -> T_Bwd_6 -> [AgdaAny] -> [AgdaAny] -> T__'8801'__12 #

d_lemma'45'bwd'45'foldr_172 :: () -> () -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Bwd_6 -> T__'8801'__12 #

d_'60''62''60''45'cancel'691'_194 :: () -> T_Bwd_6 -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 -> T__'8801'__12 #

d_'60''62''62''91''93''45'cancel'691'_232 :: () -> T_Bwd_6 -> T_Bwd_6 -> T__'8801'__12 -> T__'8801'__12 #

d_'60''62''62''45'cancel'691'_248 :: () -> T_Bwd_6 -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 -> T__'8801'__12 #

d_'60''62''62''45'cancel'737'_266 :: () -> T_Bwd_6 -> [AgdaAny] -> [AgdaAny] -> T__'8801'__12 -> T__'8801'__12 #

d_IList_302 :: p -> p -> p -> () #

data T_IList_302 #

d__'43''43'I__324 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_IList_302 -> T_IList_302 -> T_IList_302 #

du__'43''43'I__324 :: [AgdaAny] -> T_IList_302 -> T_IList_302 -> T_IList_302 #

d_lengthT_340 :: () -> [AgdaAny] -> (AgdaAny -> ()) -> T_IList_302 -> Integer #

du_lengthT_340 :: [AgdaAny] -> Integer #

d_iGetIdx_350 :: () -> [AgdaAny] -> (AgdaAny -> ()) -> T_IList_302 -> [AgdaAny] #

du_iGetIdx_350 :: [AgdaAny] -> [AgdaAny] #

d__'58''60'I__364 :: () -> (AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> T_IList_302 -> AgdaAny -> T_IList_302 #

du__'58''60'I__364 :: [AgdaAny] -> T_IList_302 -> AgdaAny -> T_IList_302 #

d_'8759''45'injectiveI_390 :: () -> (AgdaAny -> ()) -> AgdaAny -> [AgdaAny] -> [AgdaAny] -> AgdaAny -> AgdaAny -> T_IList_302 -> T_IList_302 -> T__'8801'__12 -> T__'8801'__12 -> T_Σ_14 #

du_'8759''45'injectiveI_390 :: T_Σ_14 #

d_IBwd_396 :: p -> p -> p -> () #

data T_IBwd_396 #

d__'60''62''62'I__418 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T_IList_302 #

du__'60''62''62'I__418 :: T_Bwd_6 -> T_IBwd_396 -> T_IList_302 -> T_IList_302 #

d__'60''62''60'I__436 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T_IBwd_396 #

du__'60''62''60'I__436 :: [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T_IBwd_396 #

d_lemma'60''62'I1_458 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T__'8801'__12 #

d_lemma'60''62'I2_480 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T__'8801'__12 #

d_lemma'60''62'I2''_502 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T__'8801'__12 #

d_IBwd2IList''_520 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 -> T_IBwd_396 -> T_IList_302 #

du_IBwd2IList''_520 :: T_Bwd_6 -> T_IBwd_396 -> T_IList_302 #

d_IBwd2IList_538 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 -> T_IBwd_396 -> T_IList_302 #

du_IBwd2IList_538 :: T_Bwd_6 -> T_IBwd_396 -> T_IList_302 #

d_IList2IBwd_552 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> T_Bwd_6 -> T__'8801'__12 -> T_IList_302 -> T_IBwd_396 #

du_IList2IBwd_552 :: [AgdaAny] -> T_IList_302 -> T_IBwd_396 #

d_IBwd'60''62'IList_574 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 -> T_IBwd_396 -> T_IList_302 -> T__'8801'__12 -> T__'8801'__12 #

d_split_590 :: () -> T_Bwd_6 -> [AgdaAny] -> (AgdaAny -> ()) -> T_IList_302 -> T_Σ_14 #

du_split_590 :: T_Bwd_6 -> T_IList_302 -> T_Σ_14 #

d_bsplit_630 :: () -> T_Bwd_6 -> [AgdaAny] -> (AgdaAny -> ()) -> T_IBwd_396 -> T_Σ_14 #

du_bsplit_630 :: [AgdaAny] -> T_IBwd_396 -> T_Σ_14 #

d_inj'45'IBwd2IList_676 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IBwd_396 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d__'8803'_'60''62''62'__684 :: p -> p -> p -> p -> () #

data T__'8803'_'60''62''62'__684 #

d_lem'45''8803''45''60''62''62'_710 :: () -> [AgdaAny] -> T_Bwd_6 -> [AgdaAny] -> T__'8803'_'60''62''62'__684 -> T__'8801'__12 #

d_lem'45''8803''45''60''62''62'''_722 :: () -> [AgdaAny] -> T_Bwd_6 -> [AgdaAny] -> T__'8801'__12 -> T__'8803'_'60''62''62'__684 #

du_lem'45''8803''45''60''62''62'''_722 :: T_Bwd_6 -> T__'8803'_'60''62''62'__684 #

d_done'45''8803''45''60''62''62'_734 :: () -> [AgdaAny] -> T__'8803'_'60''62''62'__684 #

du_done'45''8803''45''60''62''62'_734 :: [AgdaAny] -> T__'8803'_'60''62''62'__684 #

d_no'45'empty'45''8803''45''60''62''62'_744 :: () -> T_Bwd_6 -> AgdaAny -> [AgdaAny] -> T__'8803'_'60''62''62'__684 -> T_Irrelevant_20 #

d_unique'45''8803''45''60''62''62'_760 :: () -> [AgdaAny] -> T_Bwd_6 -> [AgdaAny] -> T__'8803'_'60''62''62'__684 -> T__'8803'_'60''62''62'__684 -> T__'8801'__12 #

d_lemma'45''8803''45''60''62''62''45'refl_780 :: () -> T_Bwd_6 -> [AgdaAny] -> T__'8803'_'60''62''62'__684 #

du_lemma'45''8803''45''60''62''62''45'refl_780 :: T_Bwd_6 -> T__'8803'_'60''62''62'__684 #

d_IIList_802 :: p -> p -> p -> p -> p -> () #

data T_IIList_802 #

d_IIBwd_832 :: p -> p -> p -> p -> p -> () #

data T_IIBwd_832 #

d__'60''62''62'II__870 :: () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T_IIBwd_832 -> T_IIList_802 -> T_IIList_802 #

du__'60''62''62'II__870 :: T_Bwd_6 -> T_IBwd_396 -> T_IIBwd_832 -> T_IIList_802 -> T_IIList_802 #

d_IIBwd2IIList_902 :: () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T__'8801'__12 -> T__'8801'__12 -> T_IIBwd_832 -> T_IIList_802 #

du_IIBwd2IIList_902 :: T_Bwd_6 -> T_IBwd_396 -> T_IIBwd_832 -> T_IIList_802 #

d_splitI_924 :: () -> T_Bwd_6 -> [AgdaAny] -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IBwd_396 -> T_IList_302 -> T_IIList_802 -> T_Σ_14 #

du_splitI_924 :: T_Bwd_6 -> T_IBwd_396 -> T_IIList_802 -> T_Σ_14 #

d_bsplitI_974 :: () -> T_Bwd_6 -> [AgdaAny] -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IBwd_396 -> T_IList_302 -> T_IIBwd_832 -> T_Σ_14 #

du_bsplitI_974 :: [AgdaAny] -> T_IList_302 -> T_IIBwd_832 -> T_Σ_14 #

d_proj'45'IIList_1028 :: () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T_IIList_802 -> AgdaAny #

du_proj'45'IIList_1028 :: T_Bwd_6 -> T_IBwd_396 -> T_IIList_802 -> AgdaAny #

d_proj'45'IIBwd_1074 :: () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T_IIBwd_832 -> AgdaAny #

du_proj'45'IIBwd_1074 :: [AgdaAny] -> T_IList_302 -> T_IIBwd_832 -> AgdaAny #

d__'8803'I_'60''62''62'__1110 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

data T__'8803'I_'60''62''62'__1110 #

d_lem'45''8803'I'45''60''62''62'1_1156 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> T_IList_302 -> T_Bwd_6 -> T_IBwd_396 -> [AgdaAny] -> T_IList_302 -> T__'8803'_'60''62''62'__684 -> T__'8803'I_'60''62''62'__1110 -> T__'8801'__12 #

d_lem'45''8803'I'45''60''62''62'1''_1178 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> T_IList_302 -> T_Bwd_6 -> T_IBwd_396 -> [AgdaAny] -> T_IList_302 -> T__'8803'_'60''62''62'__684 -> T__'8803'I_'60''62''62'__1110 -> T__'8801'__12 #

d_lem'45''8803'I'45''60''62''62'2_1200 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> T_IList_302 -> T_Bwd_6 -> T_IBwd_396 -> [AgdaAny] -> T_IList_302 -> T__'8801'__12 -> T__'8801'__12 -> T__'8803'I_'60''62''62'__1110 #

du_lem'45''8803'I'45''60''62''62'2_1200 :: T_Bwd_6 -> T_IBwd_396 -> T__'8803'I_'60''62''62'__1110 #

d_lem'45''8803'I'45''60''62''62'2''_1224 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> T_IList_302 -> T_Bwd_6 -> T_IBwd_396 -> [AgdaAny] -> T_IList_302 -> T__'8801'__12 -> T__'8801'__12 -> T__'8803'I_'60''62''62'__1110 #

du_lem'45''8803'I'45''60''62''62'2''_1224 :: T_Bwd_6 -> T_IBwd_396 -> T__'8803'I_'60''62''62'__1110 #

d_done'45''8803'I'45''60''62''62'_1238 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> T_IList_302 -> T__'8803'I_'60''62''62'__1110 #

du_done'45''8803'I'45''60''62''62'_1238 :: [AgdaAny] -> T_IList_302 -> T__'8803'I_'60''62''62'__1110 #

d_lemma'60''62'I3_1252 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> T_IBwd_396 -> T_IList_302 -> T__'8801'__12 -> T__'8801'__12 #

d_lem'45''60''62''60'I'45'subst_1272 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> T_IList_302 -> T__'8801'__12 -> T__'8801'__12 #

d_lemma'45''60''62''62'I'45''43''43'I_1290 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T_IList_302 -> T__'8801'__12 #

d_'60''62''62'I'91''93''45'cancel'691'_1314 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> T_IBwd_396 -> T_IBwd_396 -> T__'8801'__12 -> T__'8801'__12 #

d_'60''62''62'I'45'cancel'737'_1336 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> [AgdaAny] -> T_IBwd_396 -> T_IList_302 -> T_IList_302 -> T__'8801'__12 -> T__'8801'__12 #

d_equalbyPredicate'43''43'_1394 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T_IList_302 -> T_IList_302 -> (AgdaAny -> T_Irrelevant_20) -> (AgdaAny -> T_Irrelevant_20) -> T__'8801'__12 #

d_equalbyPredicate_1500 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> T_Bwd_6 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T_IBwd_396 -> T_IBwd_396 -> (AgdaAny -> T_Irrelevant_20) -> (AgdaAny -> T_Irrelevant_20) -> T__'8801'__12 #

d_equalbyPredicate'43''43'I_1588 :: () -> (AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_IList_302 -> T_IList_302 -> T_IList_302 -> T_IList_302 -> T_IList_302 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> ()) -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 -> T_IIList_802 -> T_IIList_802 -> (AgdaAny -> T_Irrelevant_20) -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14 #

du_equalbyPredicate'43''43'I_1588 :: [AgdaAny] -> [AgdaAny] -> T_IList_302 -> T_IList_302 -> T_IIList_802 -> T_IIList_802 -> T_Σ_14 #

d_equalbyPredicateI_1810 :: () -> (AgdaAny -> ()) -> T_Bwd_6 -> T_Bwd_6 -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_IList_302 -> T_IBwd_396 -> T_IBwd_396 -> T_IList_302 -> T_IList_302 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> ()) -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 -> T_IIBwd_832 -> T_IIBwd_832 -> (AgdaAny -> T_Irrelevant_20) -> (AgdaAny -> T_Irrelevant_20) -> T_Σ_14 #

du_equalbyPredicateI_1810 :: T_Bwd_6 -> T_Bwd_6 -> T_IBwd_396 -> T_IBwd_396 -> T_IIBwd_832 -> T_IIBwd_832 -> T_Σ_14 #