Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Documentation
d__DistributesOver__10 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #
d__DistributesOver'691'__12 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #
d__DistributesOver'737'__14 ∷ (Integer → Integer → Integer) → (Integer → Integer → Integer) → () Source #
d_IsCommutativeMonoid_144 ∷ p → p → () Source #
d_IsCommutativeSemigroup_148 ∷ p → () Source #
d_IsCommutativeSemiring_150 ∷ p → p → p → p → () Source #
d_IsCommutativeSemiringWithoutOne_152 ∷ p → p → p → () Source #
d_IsMagma_176 ∷ p → () Source #
d_IsMonoid_182 ∷ p → p → () Source #
d_IsSemigroup_204 ∷ p → () Source #
d_IsSemiring_208 ∷ p → p → p → p → () Source #
d_IsSemiringWithoutOne_212 ∷ p → p → p → () Source #
d_'42''45'comm_814 ∷ T_IsCommutativeSemiringWithoutOne_1382 → Integer → Integer → T__'8801'__12 Source #
d_isSemiringWithoutOne_850 ∷ T_IsCommutativeSemiringWithoutOne_1382 → T_IsSemiringWithoutOne_1298 Source #
d_'8729''45'cong_1490 ∷ T_IsMagma_176 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_isSemiringWithoutAnnihilatingZero_2448 ∷ T_IsSemiring_1570 → T_IsSemiringWithoutAnnihilatingZero_1468 Source #
d_'42''45'assoc_2546 ∷ T_IsSemiringWithoutOne_1298 → Integer → Integer → Integer → T__'8801'__12 Source #
d_'42''45'cong_2548 ∷ T_IsSemiringWithoutOne_1298 → Integer → Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_'43''45'isCommutativeMonoid_2562 ∷ T_IsSemiringWithoutOne_1298 → T_IsCommutativeMonoid_736 Source #
d_'8801''45'irrelevant_2694 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_'8804''45'antisym_2778 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #
d_'8804''45'trans_2784 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8804''45'irrelevant_2796 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #
d_s'8804's'45'injective_2834 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #
d_'60''8658''8802'_2858 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #
d_'62''8658''8802'_2862 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #
d_'8804''8658''8815'_2864 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T_Irrelevant_20 Source #
d_'60''8658''8817'_2870 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T_Irrelevant_20 Source #
d_'60''8658''8815'_2876 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T_Irrelevant_20 Source #
d_'8816''8658''8814'_2882 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8804'__22 → T_Irrelevant_20 Source #
d_'8816''8658''62'_2888 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8804'__22 Source #
d_'8816''8658''8805'_2900 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8804'__22 Source #
d_'8814''8658''8805'_2902 ∷ Integer → Integer → (T__'8804'__22 → T_Irrelevant_20) → T__'8804'__22 Source #
d_'8804''8743''8802''8658''60'_2918 ∷ Integer → Integer → T__'8804'__22 → (T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #
d_'8804''8743''8814''8658''8801'_2936 ∷ Integer → Integer → T__'8804'__22 → (T__'8804'__22 → T_Irrelevant_20) → T__'8801'__12 Source #
d_'60''45'irrefl_2970 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__22 → T_Irrelevant_20 Source #
d_'60''45'trans_2980 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8804''45''60''45'trans_2986 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'60''45''8804''45'trans_2992 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'60''45'irrelevant_3038 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 Source #
d_s'60's'45'injective_3058 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #
d_m'60'n'8658'n'8802'0_3098 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #
d_m'60'1'43'n'8658'm'60'n'8744'm'8801'n_3108 ∷ Integer → Integer → T__'8804'__22 → T__'8846'__30 Source #
d_m'8804'n'8658'm'60'n'8744'm'8801'n_3118 ∷ Integer → Integer → T__'8804'__22 → T__'8846'__30 Source #
d_'8704''91'm'8804'n'8658'm'8802'o'93''8658'n'60'o_3132 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #
du_'8704''91'm'8804'n'8658'm'8802'o'93''8658'n'60'o_3132 ∷ Integer → Integer → T__'8804'__22 Source #
d_rec_3150 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #
d_'8704''91'm'60'n'8658'm'8802'o'93''8658'n'8804'o_3160 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #
du_'8704''91'm'60'n'8658'm'8802'o'93''8658'n'8804'o_3160 ∷ Integer → Integer → T__'8804'__22 Source #
d_rec_3180 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #
d__IsRelatedTo__3188 ∷ p → p → () Source #
d_'60''45'go_3192 ∷ Integer → Integer → Integer → T__'8804'__22 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #
d_IsEquality_3194 ∷ p → p → p → () Source #
d_IsStrict_3198 ∷ p → p → p → () Source #
d_begin'45'contradiction__3204 ∷ Integer → T__IsRelatedTo__78 → AgdaAny → T_Level_18 → () → AgdaAny Source #
d_extractEquality_3214 ∷ Integer → Integer → T__IsRelatedTo__78 → T_IsEquality_208 → T__'8801'__12 Source #
d_extractStrict_3216 ∷ Integer → Integer → T__IsRelatedTo__78 → T_IsStrict_172 → T__'8804'__22 Source #
d_step'45''60'_3226 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8804'__22 → T__IsRelatedTo__78 Source #
d_step'45''8801'_3228 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #
d_step'45''8801''45''8739'_3230 ∷ Integer → Integer → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #
d_step'45''8801''45''10216'_3232 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #
d_step'45''8801''45''10217'_3234 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #
d_step'45''8801''728'_3236 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8801'__12 → T__IsRelatedTo__78 Source #
d_step'45''8804'_3238 ∷ Integer → Integer → Integer → T__IsRelatedTo__78 → T__'8804'__22 → T__IsRelatedTo__78 Source #
d_'8776''45'go_3246 ∷ Integer → Integer → Integer → T__'8801'__12 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #
d_'8801''45'go_3248 ∷ Integer → Integer → Integer → T__'8801'__12 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #
d_'8804''45'go_3250 ∷ Integer → Integer → Integer → T__'8804'__22 → T__IsRelatedTo__78 → T__IsRelatedTo__78 Source #
d_'43''45'cancel'737''45''8801'_3304 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #
d_'43''45'cancel'691''45''8801'_3312 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #
d_'43''45'cancel'737''45''8804'_3414 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'cancel'691''45''8804'_3422 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'cancel'737''45''60'_3434 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'cancel'691''45''60'_3444 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'8804'n'8658'm'8804'o'43'n_3458 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'8804'n'8658'm'8804'n'43'o_3468 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'43'n'8804'o'8658'm'8804'o_3508 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'43'n'8804'o'8658'n'8804'o_3522 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'mono'45''8804'_3530 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'mono'737''45''8804'_3544 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'mono'691''45''8804'_3554 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'mono'45''60''45''8804'_3560 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'mono'45''8804''45''60'_3570 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
du_'43''45'mono'45''8804''45''60'_3570 ∷ Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'mono'45''60'_3580 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'mono'737''45''60'_3588 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'43''45'mono'691''45''60'_3596 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'cancel'691''45''8801'_3780 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8801'__12 → T__'8801'__12 Source #
d_'42''45'cancel'737''45''8801'_3802 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8801'__12 → T__'8801'__12 Source #
d_m'42'n'8801'0'8658'm'8801'0'8744'n'8801'0_3822 ∷ Integer → Integer → T__'8801'__12 → T__'8846'__30 Source #
d_m'42'n'8801'0'8658'm'8801'0_3872 ∷ Integer → Integer → T_NonZero_112 → T__'8801'__12 → T__'8801'__12 Source #
d_'91'm'42'n'93''42''91'o'42'p'93''8801''91'm'42'o'93''42''91'n'42'p'93'_3910 ∷ Integer → Integer → Integer → Integer → T__'8801'__12 Source #
d_m'8802'0'8743'n'62'1'8658'm'42'n'62'1_3998 ∷ Integer → Integer → T_NonZero_112 → T_NonTrivial_152 → T_NonTrivial_152 Source #
d_n'8802'0'8743'm'62'1'8658'm'42'n'62'1_4012 ∷ Integer → Integer → T_NonZero_112 → T_NonTrivial_152 → T_NonTrivial_152 Source #
d_'42''45'cancel'691''45''8804'_4030 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'cancel'737''45''8804'_4044 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'mono'45''8804'_4060 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
du_'42''45'mono'45''8804'_4060 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'mono'737''45''8804'_4070 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'mono'691''45''8804'_4080 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'mono'45''60'_4086 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
du_'42''45'mono'45''60'_4086 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'mono'737''45''60'_4100 ∷ Integer → T_NonZero_112 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
du_'42''45'mono'737''45''60'_4100 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'mono'691''45''60'_4114 ∷ Integer → T_NonZero_112 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'60'n'8658'm'60'n'42'o_4166 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #
d_m'60'n'8658'm'60'o'42'n_4182 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #
du_m'60'n'8658'm'60'o'42'n_4182 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'cancel'691''45''60'_4192 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'42''45'cancel'737''45''60'_4208 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'94'n'8801'1'8658'n'8801'0'8744'm'8801'1_4308 ∷ Integer → Integer → T__'8801'__12 → T__'8846'__30 Source #
d_'94''45'mono'737''45''8804'_4346 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'94''45'mono'691''45''8804'_4360 ∷ Integer → T_NonZero_112 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
du_'94''45'mono'691''45''8804'_4360 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'94''45'mono'737''45''60'_4376 ∷ Integer → T_NonZero_112 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
du_'94''45'mono'737''45''60'_4376 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'94''45'mono'691''45''60'_4388 ∷ Integer → T__'8804'__22 → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_x'8804'y'8658'x'8851'z'8804'y_4506 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_x'8804'y'8658'z'8851'x'8804'y_4508 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_x'8804'y'8658'x'8851'z'8804'y_4510 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_x'8804'y'8658'z'8851'x'8804'y_4512 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_x'8804'y'8851'z'8658'x'8804'y_4514 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_x'8804'y'8851'z'8658'x'8804'z_4516 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_x'8804'y'8851'z'8658'x'8804'y_4534 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_x'8804'y'8851'z'8658'x'8804'z_4536 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'glb_4560 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'mono'45''8804'_4584 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'mono'691''45''8804'_4588 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'mono'737''45''8804'_4590 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'glb_4652 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'mono'45''8804'_4656 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'mono'691''45''8804'_4660 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'mono'737''45''8804'_4662 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_mono'45''8804''45'distrib'45''8852'_4728 ∷ (Integer → Integer) → (Integer → Integer → T__'8804'__22 → T__'8804'__22) → Integer → Integer → T__'8801'__12 Source #
d_mono'45''8804''45'distrib'45''8851'_4738 ∷ (Integer → Integer) → (Integer → Integer → T__'8804'__22 → T__'8804'__22) → Integer → Integer → T__'8801'__12 Source #
d_antimono'45''8804''45'distrib'45''8851'_4748 ∷ (Integer → Integer) → (Integer → Integer → T__'8804'__22 → T__'8804'__22) → Integer → Integer → T__'8801'__12 Source #
d_antimono'45''8804''45'distrib'45''8852'_4758 ∷ (Integer → Integer) → (Integer → Integer → T__'8804'__22 → T__'8804'__22) → Integer → Integer → T__'8801'__12 Source #
d_m'60'n'8658'm'60'n'8852'o_4764 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'60'n'8658'm'60'o'8852'n_4768 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'8852'n'60'o'8658'm'60'o_4776 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'8852'n'60'o'8658'n'60'o_4790 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'8852''45'mono'45''60'_4798 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8852''45'pres'45''60'm_4800 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8852''45''8851''45'isCommutativeSemiringWithoutOne_4896 ∷ T_IsCommutativeSemiringWithoutOne_1382 Source #
d_'8852''45''8851''45'commutativeSemiringWithoutOne_4898 ∷ T_CommutativeSemiringWithoutOne_2002 Source #
d_m'60'n'8658'm'8851'o'60'n_4902 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'60'n'8658'o'8851'm'60'n_4910 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'60'n'8851'o'8658'm'60'n_4920 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'60'n'8851'o'8658'm'60'o_4926 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'mono'45''60'_4928 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'pres'45'm'60'_4930 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8760''45'mono_5076 ∷ Integer → Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8760''45'mono'737''45''8804'_5090 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'8760''45'mono'691''45''8804'_5098 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'8760''45'mono'737''45''60'_5108 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
du_'8760''45'mono'737''45''60'_5108 ∷ Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8760''45'mono'691''45''60'_5134 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8760''45'cancel'691''45''8804'_5156 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8760''45'cancel'691''45''60'_5176 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_'8760''45'cancel'737''45''8801'_5196 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #
d_'8760''45'cancel'691''45''8801'_5212 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8801'__12 → T__'8801'__12 Source #
d_m'8760'n'8802'0'8658'n'60'm_5246 ∷ Integer → Integer → (T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #
d_m'62'n'8658'm'8760'n'8802'0_5274 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20 Source #
d_'43''45''8760''45'comm_5290 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #
d_'43''45''8760''45'assoc_5332 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #
d_m'8804'n'43'o'8658'm'8760'n'8804'o_5354 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
du_m'8804'n'43'o'8658'm'8760'n'8804'o_5354 ∷ Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'60'n'43'o'8658'm'8760'n'60'o_5374 ∷ Integer → Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #
d_m'43'n'8804'o'8658'm'8804'o'8760'n_5398 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 Source #
d_m'8804'o'8760'n'8658'm'43'n'8804'o_5418 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'91'm'43'n'93''8760''91'm'43'o'93''8801'n'8760'o_5520 ∷ Integer → Integer → Integer → T__'8801'__12 Source #
d_'8760''45'distrib'737''45''8851''45''8852'_5606 ∷ Integer → Integer → Integer → T__'8801'__12 Source #
d_'8760''45'distrib'737''45''8852''45''8851'_5628 ∷ Integer → Integer → Integer → T__'8801'__12 Source #
d_pred'45'mono'45''60'_5680 ∷ Integer → Integer → T_NonZero_112 → T__'8804'__22 → T__'8804'__22 Source #
d_pred'45'injective_5688 ∷ Integer → Integer → T_NonZero_112 → T_NonZero_112 → T__'8801'__12 → T__'8801'__12 Source #
d_m'8801'n'8658''8739'm'45'n'8739''8801'0_5696 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #
d_'8739'm'45'n'8739''8801'0'8658'm'8801'n_5700 ∷ Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #
d_m'8804'n'8658''8739'n'45'm'8739''8801'n'8760'm_5710 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #
d_m'8804'n'8658''8739'm'45'n'8739''8801'n'8760'm_5716 ∷ Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #
d_'8739'm'45'n'8739''8801'm'8760'n'8658'n'8804'm_5722 ∷ Integer → Integer → T__'8801'__12 → T__'8804'__22 Source #
d_'8739'm'43'n'45'm'43'o'8739''8801''8739'n'45'o'8739'_5760 ∷ Integer → Integer → Integer → T__'8801'__12 Source #
d_'8739'm'45'n'8739''8801''91'm'8760'n'93''8744''91'n'8760'm'93'_5840 ∷ Integer → Integer → T__'8846'__30 Source #
d_'42''45'distrib'737''45''8739''45''8739''45'aux_5868 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8801'__12 Source #
d_'42''45'distrib'737''45''8739''45''8739'_5880 ∷ Integer → Integer → Integer → T__'8801'__12 Source #
d_'42''45'distrib'691''45''8739''45''8739'_5910 ∷ Integer → Integer → Integer → T__'8801'__12 Source #
d_'8804''8242''45'trans_6108 ∷ Integer → Integer → Integer → T__'8804''8242'__338 → T__'8804''8242'__338 → T__'8804''8242'__338 Source #
du_'8804''8242''45'trans_6108 ∷ T__'8804''8242'__338 → T__'8804''8242'__338 → T__'8804''8242'__338 Source #
d_'8804''8242''45'step'45'injective_6136 ∷ Integer → Integer → T__'8804''8242'__338 → T__'8804''8242'__338 → T__'8801'__12 → T__'8801'__12 Source #
d_m'60'1'43'n'8658'm'60'n'8744'm'8801'n'8242'_6154 ∷ Integer → Integer → T__'8804'__22 → T__'8846'__30 Source #
d_m'8804'n'8658''8707''91'o'93'm'43'o'8801'n_6238 ∷ Integer → Integer → T__'8804'__22 → T_Σ_14 Source #
d_m'60''7495'n'8658'1'43'm'43''91'n'45'1'43'm'93''8801'n_6258 ∷ Integer → Integer → AgdaAny → T__'8801'__12 Source #
d_'8804''8243''45'irrelevant_6308 ∷ Integer → Integer → T__'8739''737'__26 → T__'8739''737'__26 → T__'8801'__12 Source #
d_'60''8243''45'irrelevant_6322 ∷ Integer → Integer → T__'8739''737'__26 → T__'8739''737'__26 → T__'8801'__12 Source #
d_'62''8243''45'irrelevant_6324 ∷ Integer → Integer → T__'8739''737'__26 → T__'8739''737'__26 → T__'8801'__12 Source #
d_'8805''8243''45'irrelevant_6326 ∷ Integer → Integer → T__'8739''737'__26 → T__'8739''737'__26 → T__'8801'__12 Source #
d_'8804''8244''8658''8804''8243'_6332 ∷ Integer → Integer → T__'8804''8244'__408 → T__'8739''737'__26 Source #
d_m'8804''8244'm'43'k_6346 ∷ Integer → Integer → Integer → T__'8801'__12 → T__'8804''8244'__408 Source #
d_'8804''8243''8658''8804''8244'_6362 ∷ Integer → Integer → T__'8739''737'__26 → T__'8804''8244'__408 Source #
d_eq'63'_6406 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → AgdaAny → T_Dec_20 Source #
d_anyUpTo'63'_6424 ∷ T_Level_18 → (Integer → ()) → (Integer → T_Dec_20) → Integer → T_Dec_20 Source #
d_'172'Pn'60'1'43'v_6458 ∷ T_Level_18 → (Integer → ()) → (Integer → T_Dec_20) → Integer → (AgdaAny → T_Irrelevant_20) → (T_Σ_14 → T_Irrelevant_20) → T_Σ_14 → T_Irrelevant_20 Source #
d_allUpTo'63'_6488 ∷ T_Level_18 → (Integer → ()) → (Integer → T_Dec_20) → Integer → T_Dec_20 Source #
d_Pn'60'1'43'v_6520 ∷ T_Level_18 → (Integer → ()) → (Integer → T_Dec_20) → Integer → AgdaAny → (Integer → T__'8804'__22 → AgdaAny) → Integer → T__'8804'__22 → AgdaAny Source #
du_Pn'60'1'43'v_6520 ∷ Integer → AgdaAny → (Integer → T__'8804'__22 → AgdaAny) → Integer → T__'8804'__22 → AgdaAny Source #
d_'8704''91'm'8804'n'8658'm'8802'o'93''8658'o'60'n_6546 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #
d_'8704''91'm'60'n'8658'm'8802'o'93''8658'o'8804'n_6554 ∷ Integer → Integer → (Integer → T__'8804'__22 → T__'8801'__12 → T_Irrelevant_20) → T__'8804'__22 Source #
d_'8739'm'43'n'45'm'43'o'8739''8801''8739'n'45'o'124'_6564 ∷ Integer → Integer → Integer → T__'8801'__12 Source #
d_'8852''45'least_6576 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'greatest_6578 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8852''45'pres'45''8804'm_6580 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_'8851''45'pres'45'm'8804'_6582 ∷ Integer → Integer → Integer → T__'8804'__22 → T__'8804'__22 → T__'8804'__22 Source #
d_suc'91'pred'91'n'93''93''8801'n_6588 ∷ Integer → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #