Documentation

d__'47'__56 ∷ Integer → Integer → AgdaAny → Integer Source #

du__'47'__56 ∷ Integer → Integer → Integer Source #

d__'37'__68 ∷ Integer → Integer → AgdaAny → Integer Source #

du__'37'__68 ∷ Integer → Integer → Integer Source #

d_m'8801'm'37'n'43''91'm'47'n'93''42'n_78 ∷ Integer → Integer → T__'8801'__12 Source #

d_m'37'n'8801'm'8760'm'47'n'42'n_88 ∷ Integer → Integer → T__'8801'__12 Source #

d_n_98 ∷ Integer → Integer → Integer Source #

du_n_98 ∷ Integer → Integer Source #

d_m'47'n'42'n_100 ∷ Integer → Integer → Integer Source #

d_n'37'1'8801'0_106 ∷ Integer → T__'8801'__12 Source #

d_n'37'n'8801'0_110 ∷ Integer → T__'8801'__12 Source #

d_m'37'n'37'n'8801'm'37'n_118 ∷ Integer → Integer → T__'8801'__12 Source #

d_'91'm'43'n'93''37'n'8801'm'37'n_128 ∷ Integer → Integer → T__'8801'__12 Source #

d_'91'm'43'kn'93''37'n'8801'm'37'n_140 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_n_158 ∷ Integer → Integer → Integer → Integer Source #

du_n_158 ∷ Integer → Integer Source #

d_m'42'n'37'n'8801'0_166 ∷ Integer → Integer → T__'8801'__12 Source #

d_m'37'n'60'n_172 ∷ Integer → Integer → T__'8804'__18 Source #

d_m'37'n'8804'm_182 ∷ Integer → Integer → T__'8804'__18 Source #

d_m'8804'n'8658'm'37'n'8801'm_192 ∷ Integer → Integer → T__'8804'__18 → T__'8801'__12 Source #

d_'37''45'pred'45''8801'0_218 ∷ Integer → Integer → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_234 ∷ Integer → Integer → Integer → AgdaAny → T__'8804'__18 → T__'8804'__18 Source #

du_m'60''91'1'43'n'37'd'93''8658'm'8804''91'n'37'd'93'_234 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_250 ∷ Integer → Integer → Integer → AgdaAny → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'91'1'43'm'37'd'93''8804'1'43'n'8658''91'm'37'd'93''8804'n_250 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'37''45'distrib'737''45''43'_268 ∷ Integer → Integer → Integer → AgdaAny → T__'8801'__12 Source #

d_'37''45'distrib'737''45''42'_298 ∷ Integer → Integer → Integer → AgdaAny → T__'8801'__12 Source #

d_m'8242'_312 ∷ Integer → Integer → Integer → T_'8868'_6 → T_'8868'_6 → Integer Source #

du_m'8242'_312 ∷ Integer → Integer → T_'8868'_6 → Integer Source #

d_n'8242'_314 ∷ Integer → Integer → Integer → T_'8868'_6 → T_'8868'_6 → Integer Source #

du_n'8242'_314 ∷ Integer → Integer → T_'8868'_6 → Integer Source #

d_k_316 ∷ Integer → Integer → Integer → T_'8868'_6 → T_'8868'_6 → Integer Source #

du_k_316 ∷ Integer → Integer → T_'8868'_6 → Integer Source #

d_j_318 ∷ Integer → Integer → Integer → T_'8868'_6 → T_'8868'_6 → Integer Source #

du_j_318 ∷ Integer → Integer → T_'8868'_6 → Integer Source #

d_lemma_320 ∷ Integer → Integer → Integer → T_'8868'_6 → T__'8801'__12 Source #

d_'37''45'remove'45''43''737'_340 ∷ Integer → Integer → Integer → AgdaAny → T__'8739'__12 → T__'8801'__12 Source #

d_'37''45'remove'45''43''691'_362 ∷ Integer → Integer → Integer → AgdaAny → T__'8739'__12 → T__'8801'__12 Source #

d_'47''45'cong'737'_382 ∷ Integer → Integer → Integer → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_'47''45'cong'691'_394 ∷ Integer → Integer → Integer → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #

d_0'47'n'8801'0_400 ∷ Integer → AgdaAny → T__'8801'__12 Source #

d_n'47'1'8801'n_406 ∷ Integer → T__'8801'__12 Source #

d_n'47'n'8801'1_414 ∷ Integer → AgdaAny → T__'8801'__12 Source #

d_m'42'n'47'n'8801'm_424 ∷ Integer → Integer → AgdaAny → T__'8801'__12 Source #

d_m'47'n'42'n'8801'm_436 ∷ Integer → Integer → AgdaAny → T__'8739'__12 → T__'8801'__12 Source #

d_m'42''91'n'47'm'93''8801'n_452 ∷ Integer → Integer → AgdaAny → T__'8739'__12 → T__'8801'__12 Source #

d_m'47'n'42'n'8804'm_464 ∷ Integer → Integer → AgdaAny → T__'8804'__18 Source #

du_m'47'n'42'n'8804'm_464 ∷ Integer → Integer → T__'8804'__18 Source #

d_m'47'n'8804'm_478 ∷ Integer → Integer → AgdaAny → T__'8804'__18 Source #

du_m'47'n'8804'm_478 ∷ Integer → Integer → T__'8804'__18 Source #

d_m'47'n'60'm_492 ∷ Integer → Integer → AgdaAny → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_m'47'n'60'm_492 ∷ Integer → Integer → T__'8804'__18 Source #

d_'47''45'mono'45''8804'_516 ∷ Integer → Integer → Integer → Integer → AgdaAny → AgdaAny → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

du_'47''45'mono'45''8804'_516 ∷ Integer → Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 → T__'8804'__18 Source #

d_'47''45'mono'737''45''8804'_530 ∷ Integer → Integer → Integer → AgdaAny → T__'8804'__18 → T__'8804'__18 Source #

du_'47''45'mono'737''45''8804'_530 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'47''45'mono'691''45''8804'_546 ∷ Integer → Integer → Integer → AgdaAny → AgdaAny → T__'8804'__18 → T__'8804'__18 Source #

du_'47''45'mono'691''45''8804'_546 ∷ Integer → Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'47''45'cancel'691''45''8801'_562 ∷ Integer → Integer → Integer → AgdaAny → T__'8739'__12 → T__'8739'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_m'60'n'8658'm'47'n'8801'0_586 ∷ Integer → Integer → AgdaAny → T__'8804'__18 → T__'8801'__12 Source #

d_m'8805'n'8658'm'47'n'62'0_602 ∷ Integer → Integer → AgdaAny → T__'8804'__18 → T__'8804'__18 Source #

du_m'8805'n'8658'm'47'n'62'0_602 ∷ Integer → Integer → T__'8804'__18 → T__'8804'__18 Source #

d_'43''45'distrib'45''47'_622 ∷ Integer → Integer → Integer → AgdaAny → T__'8804'__18 → T__'8801'__12 Source #

d_'43''45'distrib'45''47''45''8739''737'_640 ∷ Integer → Integer → Integer → AgdaAny → T__'8739'__12 → T__'8801'__12 Source #

d_'43''45'distrib'45''47''45''8739''691'_662 ∷ Integer → Integer → Integer → AgdaAny → T__'8739'__12 → T__'8801'__12 Source #

d_m'47'n'8801'1'43''91'm'8760'n'93''47'n_682 ∷ Integer → Integer → AgdaAny → T__'8804'__18 → T__'8801'__12 Source #

d_m'42'n'47'm'42'o'8801'n'47'o_706 ∷ Integer → Integer → Integer → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_helper_724 ∷ Integer → Integer → Integer → AgdaAny → AgdaAny → Integer → T_Acc_42 → T__'8801'__12 Source #

d_n'8760'o'60'n_750 ∷ Integer → Integer → (T__'8804'__18 → T_'8869'_4) → Integer → Integer → AgdaAny → AgdaAny → (Integer → T__'8804'__18 → T_Acc_42) → T__'8804'__18 Source #

du_n'8760'o'60'n_750 ∷ Integer → Integer → T__'8804'__18 Source #

d_'42''45''47''45'assoc_760 ∷ Integer → Integer → Integer → AgdaAny → T__'8739'__12 → T__'8801'__12 Source #

d_'47''45''42''45'interchange_790 ∷ Integer → Integer → Integer → Integer → AgdaAny → AgdaAny → AgdaAny → T__'8739'__12 → T__'8739'__12 → T__'8801'__12 Source #

d_DivMod_808 ∷ p → p → () Source #

data T_DivMod_808 Source #

d_quotient_820 ∷ T_DivMod_808 → Integer Source #

d_remainder_822 ∷ T_DivMod_808 → T_Fin_6 Source #

d_property_824 ∷ T_DivMod_808 → T__'8801'__12 Source #

d__div__834 ∷ Integer → Integer → AgdaAny → Integer Source #

d__mod__842 ∷ Integer → Integer → AgdaAny → T_Fin_6 Source #

du__mod__842 ∷ Integer → Integer → T_Fin_6 Source #

d__divMod__854 ∷ Integer → Integer → AgdaAny → T_DivMod_808 Source #

du__divMod__854 ∷ Integer → Integer → T_DivMod_808 Source #

d_'91'm'47'n'93''42'n_866 ∷ Integer → Integer → T_'8868'_6 → Integer Source #

du_'91'm'47'n'93''42'n_866 ∷ Integer → Integer → Integer Source #

d_a'8801'a'37'n'43''91'a'47'n'93''42'n_870 ∷ Integer → Integer → T__'8801'__12 Source #

d_a'37'1'8801'0_872 ∷ Integer → T__'8801'__12 Source #

d_a'37'n'37'n'8801'a'37'n_874 ∷ Integer → Integer → T__'8801'__12 Source #

d_'91'a'43'n'93''37'n'8801'a'37'n_876 ∷ Integer → Integer → T__'8801'__12 Source #

d_'91'a'43'kn'93''37'n'8801'a'37'n_878 ∷ Integer → Integer → Integer → T__'8801'__12 Source #

d_kn'37'n'8801'0_880 ∷ Integer → Integer → T__'8801'__12 Source #

d_a'37'n'60'n_882 ∷ Integer → Integer → T__'8804'__18 Source #