Documentation

d_quotient'8802'0_18 ∷ Integer → Integer → T__'8739'__20 → T_NonZero_112 → T_NonZero_112 Source #

du_quotient'8802'0_18 ∷ T_NonZero_112 Source #

d_m'8739'n'8658'n'8801'quotient'42'm_28 ∷ Integer → Integer → T__'8739'__20 → T__'8801'__12 Source #

d_m'8739'n'8658'n'8801'm'42'quotient_34 ∷ Integer → Integer → T__'8739'__20 → T__'8801'__12 Source #

d_quotient'45''8739'_46 ∷ Integer → Integer → T__'8739'__20 → T__'8739'__20 Source #

du_quotient'45''8739'_46 ∷ Integer → T__'8739'__20 Source #

d_quotient'62'1_54 ∷ Integer → Integer → T__'8739'__20 → T__'8804'__22 → T__'8804'__22 Source #

d_quotient'45''60'_70 ∷ Integer → Integer → T__'8739'__20 → T_NonTrivial_152 → T_NonZero_112 → T__'8804'__22 Source #

du_quotient'45''60'_70 ∷ Integer → Integer → T__'8739'__20 → T__'8804'__22 Source #

d_n'47'm'8801'quotient_88 ∷ Integer → Integer → T__'8739'__20 → T_NonZero_112 → T__'8801'__12 Source #

d_m'37'n'8801'0'8658'n'8739'm_100 ∷ Integer → Integer → T_NonZero_112 → T__'8801'__12 → T__'8739'__20 Source #

du_m'37'n'8801'0'8658'n'8739'm_100 ∷ Integer → Integer → T__'8739'__20 Source #

d_'91'm'47'n'93''42'n_112 ∷ Integer → Integer → T_NonZero_112 → T__'8801'__12 → Integer Source #

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

d_n'8739'm'8658'm'37'n'8801'0_122 ∷ Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8801'__12 Source #

d_m'37'n'8801'0'8660'n'8739'm_134 ∷ Integer → Integer → T_NonZero_112 → T_Equivalence_1714 Source #

du_m'37'n'8801'0'8660'n'8739'm_134 ∷ Integer → Integer → T_Equivalence_1714 Source #

d_'8739''8658''8804'_142 ∷ Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8804'__22 Source #

du_'8739''8658''8804'_142 ∷ Integer → T__'8739'__20 → T__'8804'__22 Source #

d_'62''8658''8740'_154 ∷ Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8739'__20 → T_Irrelevant_20 Source #

d_'8739''45'reflexive_162 ∷ Integer → Integer → T__'8801'__12 → T__'8739'__20 Source #

du_'8739''45'reflexive_162 ∷ T__'8739'__20 Source #

d_'8739''45'refl_166 ∷ Integer → T__'8739'__20 Source #

du_'8739''45'refl_166 ∷ T__'8739'__20 Source #

d_'8739''45'trans_168 ∷ Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_'8739''45'trans_168 ∷ T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_'8739''45'antisym_174 ∷ Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8801'__12 Source #

d__'8739''63'__192 ∷ Integer → Integer → T_Dec_20 Source #

d_'8739''45'isPreorder_200 ∷ T_IsPreorder_70 Source #

d_'8739''45'isPartialOrder_202 ∷ T_IsPartialOrder_174 Source #

d_'8739''45'preorder_204 ∷ T_Preorder_132 Source #

d_'8739''45'poset_206 ∷ T_Poset_314 Source #

d__IsRelatedTo__212 ∷ p → p → () Source #

d__'8718'_214 ∷ Integer → T__IsRelatedTo__62 Source #

d_IsEquality_216 ∷ p → p → p → () Source #

d_IsEquality'63'_218 ∷ Integer → Integer → T__IsRelatedTo__62 → T_Dec_20 Source #

d_begin__220 ∷ Integer → Integer → T__IsRelatedTo__62 → T__'8739'__20 Source #

d_begin__222 ∷ Integer → Integer → T__IsRelatedTo__62 → AgdaAny → T__'8801'__12 Source #

d_equalitySubRelation_224 ∷ T_SubRelation_60 Source #

d_extractEquality_228 ∷ Integer → Integer → T__IsRelatedTo__62 → T_IsEquality_122 → T__'8801'__12 Source #

d_start_234 ∷ Integer → Integer → T__IsRelatedTo__62 → T__'8739'__20 Source #

d_step'45''8801'_246 ∷ Integer → Integer → Integer → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #

d_step'45''8801''45''8739'_248 ∷ Integer → Integer → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #

du_step'45''8801''45''8739'_248 ∷ T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #

d_step'45''8801''45''10216'_250 ∷ Integer → Integer → Integer → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #

d_step'45''8801''45''10217'_252 ∷ Integer → Integer → Integer → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #

d_step'45''8801''728'_254 ∷ Integer → Integer → Integer → T__IsRelatedTo__62 → T__'8801'__12 → T__IsRelatedTo__62 Source #

d_stop_258 ∷ Integer → T__IsRelatedTo__62 Source #

d_'8776''45'go_260 ∷ Integer → Integer → Integer → T__'8801'__12 → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #

d_'8801''45'go_262 ∷ Integer → Integer → Integer → T__'8801'__12 → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #

du_'8801''45'go_262 ∷ T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #

d_'8818''45'go_264 ∷ Integer → Integer → Integer → T__'8739'__20 → T__IsRelatedTo__62 → T__IsRelatedTo__62 Source #

d_step'45''8739'_278 ∷ Integer → Integer → Integer → T__IsRelatedTo__62 → T__'8739'__20 → T__IsRelatedTo__62 Source #

d__'8739'0_282 ∷ Integer → T__'8739'__20 Source #

du__'8739'0_282 ∷ T__'8739'__20 Source #

d_0'8739''8658''8801'0_286 ∷ Integer → T__'8739'__20 → T__'8801'__12 Source #

d_1'8739'__294 ∷ Integer → T__'8739'__20 Source #

d_'8739'1'8658''8801'1_298 ∷ Integer → T__'8739'__20 → T__'8801'__12 Source #

d_n'8739'n_304 ∷ Integer → T__'8739'__20 Source #

du_n'8739'n_304 ∷ T__'8739'__20 Source #

d_'8739'm'8739'n'8658''8739'm'43'n_306 ∷ Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_'8739'm'8739'n'8658''8739'm'43'n_306 ∷ T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_'8739'm'43'n'8739'm'8658''8739'n_312 ∷ Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_'8739'm'43'n'8739'm'8658''8739'n_312 ∷ T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_n'8739'm'42'n_338 ∷ Integer → Integer → T__'8739'__20 Source #

du_n'8739'm'42'n_338 ∷ Integer → T__'8739'__20 Source #

d_m'8739'm'42'n_346 ∷ Integer → Integer → T__'8739'__20 Source #

du_m'8739'm'42'n_346 ∷ Integer → T__'8739'__20 Source #

d_n'8739'm'42'n'42'o_356 ∷ Integer → Integer → Integer → T__'8739'__20 Source #

du_n'8739'm'42'n'42'o_356 ∷ Integer → Integer → T__'8739'__20 Source #

d_'8739'm'8658''8739'm'42'n_364 ∷ Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 Source #

du_'8739'm'8658''8739'm'42'n_364 ∷ Integer → T__'8739'__20 → T__'8739'__20 Source #

d_'8739'n'8658''8739'm'42'n_374 ∷ Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 Source #

du_'8739'n'8658''8739'm'42'n_374 ∷ Integer → T__'8739'__20 → T__'8739'__20 Source #

d_m'42'n'8739''8658'm'8739'_388 ∷ Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 Source #

du_m'42'n'8739''8658'm'8739'_388 ∷ Integer → T__'8739'__20 → T__'8739'__20 Source #

d_m'42'n'8739''8658'n'8739'_400 ∷ Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 Source #

du_m'42'n'8739''8658'n'8739'_400 ∷ Integer → T__'8739'__20 → T__'8739'__20 Source #

d_'42''45'pres'45''8739'_410 ∷ Integer → Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_'42''45'pres'45''8739'_410 ∷ T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_'42''45'mono'691''45''8739'_426 ∷ Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 Source #

du_'42''45'mono'691''45''8739'_426 ∷ T__'8739'__20 → T__'8739'__20 Source #

d_'42''45'mono'737''45''8739'_432 ∷ Integer → Integer → Integer → T__'8739'__20 → T__'8739'__20 Source #

du_'42''45'mono'737''45''8739'_432 ∷ T__'8739'__20 → T__'8739'__20 Source #

d_'42''45'cancel'737''45''8739'_440 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 Source #

du_'42''45'cancel'737''45''8739'_440 ∷ T__'8739'__20 → T__'8739'__20 Source #

d_q_454 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → Integer Source #

du_q_454 ∷ T__'8739'__20 → Integer Source #

d_'42''45'cancel'691''45''8739'_462 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 Source #

du_'42''45'cancel'691''45''8739'_462 ∷ T__'8739'__20 → T__'8739'__20 Source #

d_'8739'm'8760'n'8739'n'8658''8739'm_480 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_'8739'm'8760'n'8739'n'8658''8739'm_480 ∷ T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_m'47'n'8739'm_504 ∷ Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 Source #

du_m'47'n'8739'm_504 ∷ Integer → Integer → T__'8739'__20 → T__'8739'__20 Source #

d_m'42'n'8739'o'8658'm'8739'o'47'n_522 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 Source #

du_m'42'n'8739'o'8658'm'8739'o'47'n_522 ∷ T__'8739'__20 → T__'8739'__20 Source #

d_m'42'n'8739'o'8658'n'8739'o'47'm_542 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 Source #

du_m'42'n'8739'o'8658'n'8739'o'47'm_542 ∷ T__'8739'__20 → T__'8739'__20 Source #

d_m'8739'n'47'o'8658'm'42'o'8739'n_554 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_m'8739'n'47'o'8658'm'42'o'8739'n_554 ∷ Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_m'8739'n'47'o'8658'o'42'm'8739'n_574 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_m'8739'n'47'o'8658'o'42'm'8739'n_574 ∷ Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_m'47'n'8739'o'8658'm'8739'o'42'n_586 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_m'47'n'8739'o'8658'm'8739'o'42'n_586 ∷ Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_m'8739'n'42'o'8658'm'47'n'8739'o_606 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_m'8739'n'42'o'8658'm'47'n'8739'o_606 ∷ Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_'8739'n'8739'm'37'n'8658''8739'm_624 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_'8739'n'8739'm'37'n'8658''8739'm_624 ∷ Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_'37''45'pres'737''45''8739'_648 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

du_'37''45'pres'737''45''8739'_648 ∷ Integer → Integer → T__'8739'__20 → T__'8739'__20 → T__'8739'__20 Source #

d_m'8804'n'8658'm'33''8739'n'33'_670 ∷ Integer → Integer → T__'8804'__22 → T__'8739'__20 Source #

du_m'8804'n'8658'm'33''8739'n'33'_670 ∷ Integer → T__'8804'__22 → T__'8739'__20 Source #

d_help_678 ∷ Integer → Integer → T__'8804'__22 → Integer → Integer → T__'8804''8242'__338 → T__'8739'__20 Source #

du_help_678 ∷ Integer → T__'8804''8242'__338 → T__'8739'__20 Source #

d_hasNonTrivialDivisor'45''8802'_684 ∷ Integer → Integer → T_NonTrivial_152 → T_NonZero_112 → (T__'8801'__12 → T_Irrelevant_20) → T__'8739'__20 → T__HasNonTrivialDivisorLessThan__50 Source #

du_hasNonTrivialDivisor'45''8802'_684 ∷ Integer → Integer → T__'8739'__20 → T__HasNonTrivialDivisorLessThan__50 Source #

d_hasNonTrivialDivisor'45''8739'_690 ∷ Integer → Integer → Integer → T__HasNonTrivialDivisorLessThan__50 → T__'8739'__20 → T__HasNonTrivialDivisorLessThan__50 Source #

du_hasNonTrivialDivisor'45''8739'_690 ∷ T__HasNonTrivialDivisorLessThan__50 → T__'8739'__20 → T__HasNonTrivialDivisorLessThan__50 Source #

d_hasNonTrivialDivisor'45''8804'_698 ∷ Integer → Integer → Integer → T__HasNonTrivialDivisorLessThan__50 → T__'8804'__22 → T__HasNonTrivialDivisorLessThan__50 Source #

du_hasNonTrivialDivisor'45''8804'_698 ∷ T__HasNonTrivialDivisorLessThan__50 → T__'8804'__22 → T__HasNonTrivialDivisorLessThan__50 Source #