Documentation

d_m'37'n'8801'0'8658'n'8739'm_12 :: Integer -> Integer -> T_NonZero_76 -> T__'8801'__12 -> T__'8739'__12 Source #

du_m'37'n'8801'0'8658'n'8739'm_12 :: Integer -> Integer -> T__'8739'__12 Source #

d_n'8739'm'8658'm'37'n'8801'0_30 :: Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8801'__12 Source #

d_m'37'n'8801'0'8660'n'8739'm_52 :: Integer -> Integer -> T_NonZero_76 -> T_Equivalence_928 Source #

du_m'37'n'8801'0'8660'n'8739'm_52 :: Integer -> Integer -> T_Equivalence_928 Source #

d_'8739''8658''8804'_64 :: Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8804'__18 Source #

du_'8739''8658''8804'_64 :: Integer -> Integer -> T__'8739'__12 -> T__'8804'__18 Source #

d_'62''8658''8740'_84 :: Integer -> Integer -> T_NonZero_76 -> T__'8804'__18 -> T__'8739'__12 -> T_'8869'_4 Source #

d_'8739''45'reflexive_90 :: Integer -> Integer -> T__'8801'__12 -> T__'8739'__12 Source #

du_'8739''45'reflexive_90 :: T__'8739'__12 Source #

d_'8739''45'refl_94 :: Integer -> T__'8739'__12 Source #

du_'8739''45'refl_94 :: T__'8739'__12 Source #

d_'8739''45'trans_96 :: Integer -> Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_'8739''45'trans_96 :: T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_'8739''45'antisym_102 :: Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8801'__12 Source #

d__'8739''63'__122 :: Integer -> Integer -> T_Dec_32 Source #

d_'8739''45'isPreorder_130 :: T_IsPreorder_70 Source #

d_'8739''45'isPartialOrder_132 :: T_IsPartialOrder_162 Source #

d_'8739''45'preorder_134 :: T_Preorder_132 Source #

d_'8739''45'poset_136 :: T_Poset_282 Source #

d__IsRelatedTo__142 :: p1 -> p2 -> () Source #

d__'8718'_144 :: Integer -> T__IsRelatedTo__56 Source #

d__'8776''10216''10217'__146 :: Integer -> Integer -> T__IsRelatedTo__56 -> T__IsRelatedTo__56 Source #

du__'8776''10216''10217'__146 :: T__IsRelatedTo__56 -> T__IsRelatedTo__56 Source #

d__'8801''10216''10217'__148 :: T__IsRelatedTo__56 -> T__IsRelatedTo__56 Source #

d_IsEquality_150 :: p1 -> p2 -> p3 -> () Source #

d_IsEquality'63'_152 :: Integer -> Integer -> T__IsRelatedTo__56 -> T_Dec_32 Source #

d_begin__154 :: Integer -> Integer -> T__IsRelatedTo__56 -> T__'8739'__12 Source #

d_begin'45'equality__156 :: Integer -> Integer -> T__IsRelatedTo__56 -> AgdaAny -> T__'8801'__12 Source #

d_extractEquality_160 :: Integer -> Integer -> T__IsRelatedTo__56 -> T_IsEquality_74 -> T__'8801'__12 Source #

d_step'45''8801'_172 :: Integer -> Integer -> Integer -> T__IsRelatedTo__56 -> T__'8801'__12 -> T__IsRelatedTo__56 Source #

du_step'45''8801'_172 :: T__IsRelatedTo__56 -> T__IsRelatedTo__56 Source #

d_step'45''8801''728'_174 :: Integer -> Integer -> Integer -> T__IsRelatedTo__56 -> T__'8801'__12 -> T__IsRelatedTo__56 Source #

du_step'45''8801''728'_174 :: T__IsRelatedTo__56 -> T__IsRelatedTo__56 Source #

d_step'45''8739'_186 :: Integer -> Integer -> Integer -> T__IsRelatedTo__56 -> T__'8739'__12 -> T__IsRelatedTo__56 Source #

d_1'8739'__190 :: Integer -> T__'8739'__12 Source #

d__'8739'0_196 :: Integer -> T__'8739'__12 Source #

du__'8739'0_196 :: T__'8739'__12 Source #

d_0'8739''8658''8801'0_202 :: Integer -> T__'8739'__12 -> T__'8801'__12 Source #

d_'8739'1'8658''8801'1_210 :: Integer -> T__'8739'__12 -> T__'8801'__12 Source #

d_n'8739'n_218 :: Integer -> T__'8739'__12 Source #

du_n'8739'n_218 :: T__'8739'__12 Source #

d_'8739'm'8739'n'8658''8739'm'43'n_228 :: Integer -> Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_'8739'm'8739'n'8658''8739'm'43'n_228 :: T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_'8739'm'43'n'8739'm'8658''8739'n_240 :: Integer -> Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_'8739'm'43'n'8739'm'8658''8739'n_240 :: T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_n'8739'm'42'n_266 :: Integer -> Integer -> T__'8739'__12 Source #

du_n'8739'm'42'n_266 :: Integer -> T__'8739'__12 Source #

d_m'8739'm'42'n_274 :: Integer -> Integer -> T__'8739'__12 Source #

du_m'8739'm'42'n_274 :: Integer -> T__'8739'__12 Source #

d_n'8739'm'42'n'42'o_284 :: Integer -> Integer -> Integer -> T__'8739'__12 Source #

du_n'8739'm'42'n'42'o_284 :: Integer -> Integer -> T__'8739'__12 Source #

d_'8739'm'8658''8739'm'42'n_296 :: Integer -> Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 Source #

du_'8739'm'8658''8739'm'42'n_296 :: Integer -> T__'8739'__12 -> T__'8739'__12 Source #

d_'8739'n'8658''8739'm'42'n_312 :: Integer -> Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 Source #

du_'8739'n'8658''8739'm'42'n_312 :: Integer -> T__'8739'__12 -> T__'8739'__12 Source #

d_'42''45'mono'691''45''8739'_330 :: Integer -> Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 Source #

du_'42''45'mono'691''45''8739'_330 :: T__'8739'__12 -> T__'8739'__12 Source #

d_'42''45'mono'737''45''8739'_352 :: Integer -> Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 Source #

du_'42''45'mono'737''45''8739'_352 :: T__'8739'__12 -> T__'8739'__12 Source #

d_'42''45'cancel'737''45''8739'_376 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 Source #

du_'42''45'cancel'737''45''8739'_376 :: T__'8739'__12 -> T__'8739'__12 Source #

d_'42''45'cancel'691''45''8739'_402 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 Source #

du_'42''45'cancel'691''45''8739'_402 :: T__'8739'__12 -> T__'8739'__12 Source #

d_'8739'm'8760'n'8739'n'8658''8739'm_424 :: Integer -> Integer -> Integer -> T__'8804'__18 -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_'8739'm'8760'n'8739'n'8658''8739'm_424 :: T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_m'47'n'8739'm_452 :: Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 Source #

du_m'47'n'8739'm_452 :: Integer -> T__'8739'__12 -> T__'8739'__12 Source #

d_m'42'n'8739'o'8658'm'8739'o'47'n_472 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 Source #

du_m'42'n'8739'o'8658'm'8739'o'47'n_472 :: Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 Source #

d_m'42'n'8739'o'8658'n'8739'o'47'm_496 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 Source #

du_m'42'n'8739'o'8658'n'8739'o'47'm_496 :: Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 Source #

d_m'8739'n'47'o'8658'm'42'o'8739'n_514 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_m'8739'n'47'o'8658'm'42'o'8739'n_514 :: Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_m'8739'n'47'o'8658'o'42'm'8739'n_540 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_m'8739'n'47'o'8658'o'42'm'8739'n_540 :: Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_m'47'n'8739'o'8658'm'8739'o'42'n_558 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_m'47'n'8739'o'8658'm'8739'o'42'n_558 :: Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_m'8739'n'42'o'8658'm'47'n'8739'o_582 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_m'8739'n'42'o'8658'm'47'n'8739'o_582 :: Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_'8739'n'8739'm'37'n'8658''8739'm_604 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_'8739'n'8739'm'37'n'8658''8739'm_604 :: Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_'37''45'pres'737''45''8739'_636 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

du_'37''45'pres'737''45''8739'_636 :: Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 -> T__'8739'__12 Source #

d_ad'47'n_654 :: Integer -> Integer -> T_NonZero_76 -> Integer -> Integer -> T__'8801'__12 -> T_NonZero_76 -> Integer Source #

du_ad'47'n_654 :: Integer -> Integer -> Integer -> T_NonZero_76 -> Integer Source #

d_poset_660 :: T_Poset_282 Source #

d_'42''45'cong_662 :: Integer -> Integer -> Integer -> T__'8739'__12 -> T__'8739'__12 Source #

du_'42''45'cong_662 :: T__'8739'__12 -> T__'8739'__12 Source #

d_'47''45'cong_664 :: Integer -> Integer -> Integer -> T_NonZero_76 -> T__'8739'__12 -> T__'8739'__12 Source #

du_'47''45'cong_664 :: T__'8739'__12 -> T__'8739'__12 Source #