Documentation

d__Absorbs__8 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → () Source #

d__DistributesOver__10 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → () Source #

d__DistributesOver'691'__12 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → () Source #

d__DistributesOver'737'__14 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → () Source #

d__IdempotentOn__16 ∷ (Bool → Bool → Bool) → Bool → () Source #

d_Absorptive_18 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → () Source #

d_Associative_26 ∷ (Bool → Bool → Bool) → () Source #

d_Commutative_30 ∷ (Bool → Bool → Bool) → () Source #

d_Idempotent_38 ∷ (Bool → Bool → Bool) → () Source #

d_Identity_42 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_Inverse_46 ∷ Bool → (Bool → Bool) → (Bool → Bool → Bool) → () Source #

d_Involutive_48 ∷ (Bool → Bool) → () Source #

d_LeftIdentity_56 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_LeftInverse_58 ∷ Bool → (Bool → Bool) → (Bool → Bool → Bool) → () Source #

d_LeftZero_60 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_RightIdentity_68 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_RightInverse_70 ∷ Bool → (Bool → Bool) → (Bool → Bool → Bool) → () Source #

d_RightZero_72 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_Selective_74 ∷ (Bool → Bool → Bool) → () Source #

d_Zero_76 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_IsAbelianGroup_80 ∷ p → p → p → () Source #

d_IsBand_82 ∷ p → () Source #

d_IsBooleanAlgebra_84 ∷ p → p → p → p → p → () Source #

d_IsCancellativeCommutativeSemiring_88 ∷ p → p → p → p → () Source #

d_IsCommutativeMagma_90 ∷ p → () Source #

d_IsCommutativeMonoid_92 ∷ p → p → () Source #

d_IsCommutativeRing_94 ∷ p → p → p → p → p → () Source #

d_IsCommutativeSemigroup_96 ∷ p → () Source #

d_IsCommutativeSemiring_98 ∷ p → p → p → p → () Source #

d_IsCommutativeSemiringWithoutOne_100 ∷ p → p → p → () Source #

d_IsDistributiveLattice_102 ∷ p → p → () Source #

d_IsGroup_104 ∷ p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_106 ∷ p → p → () Source #

d_IsLattice_108 ∷ p → p → () Source #

d_IsMagma_110 ∷ p → () Source #

d_IsMonoid_112 ∷ p → p → () Source #

d_IsNearSemiring_114 ∷ p → p → p → () Source #

d_IsRing_116 ∷ p → p → p → p → p → () Source #

d_IsSelectiveMagma_118 ∷ p → () Source #

d_IsSemigroup_120 ∷ p → () Source #

d_IsSemilattice_122 ∷ p → () Source #

d_IsSemiring_124 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_126 ∷ p → p → p → p → () Source #

d_IsSemiringWithoutOne_128 ∷ p → p → p → () Source #

d_assoc_134 ∷ T_IsAbelianGroup_662 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_136 ∷ T_IsAbelianGroup_662 → Bool → Bool → T__'8801'__12 Source #

d_identity_138 ∷ T_IsAbelianGroup_662 → T_Σ_14 Source #

d_inverse_144 ∷ T_IsAbelianGroup_662 → T_Σ_14 Source #

d_isEquivalence_156 ∷ T_IsAbelianGroup_662 → T_IsEquivalence_26 Source #

d_isGroup_158 ∷ T_IsAbelianGroup_662 → T_IsGroup_580 Source #

d_isMagma_160 ∷ T_IsAbelianGroup_662 → T_IsMagma_86 Source #

d_isMonoid_162 ∷ T_IsAbelianGroup_662 → T_IsMonoid_358 Source #

d_isSemigroup_166 ∷ T_IsAbelianGroup_662 → T_IsSemigroup_194 Source #

d_'8315''185''45'cong_182 ∷ T_IsAbelianGroup_662 → Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_184 ∷ T_IsAbelianGroup_662 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_192 ∷ T_IsBand_230 → Bool → Bool → Bool → T__'8801'__12 Source #

d_idem_194 ∷ T_IsBand_230 → Bool → T__'8801'__12 Source #

d_isEquivalence_196 ∷ T_IsBand_230 → T_IsEquivalence_26 Source #

d_isMagma_198 ∷ T_IsBand_230 → T_IsMagma_86 Source #

d_isSemigroup_202 ∷ T_IsBand_230 → T_IsSemigroup_194 Source #

d_'8729''45'cong_214 ∷ T_IsBand_230 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_absorptive_222 ∷ T_IsBooleanAlgebra_1864 → T_Σ_14 Source #

d_isDistributiveLattice_224 ∷ T_IsBooleanAlgebra_1864 → T_IsDistributiveLattice_814 Source #

d_isEquivalence_226 ∷ T_IsBooleanAlgebra_1864 → T_IsEquivalence_26 Source #

d_isLattice_228 ∷ T_IsBooleanAlgebra_1864 → T_IsLattice_740 Source #

d_'172''45'cong_240 ∷ T_IsBooleanAlgebra_1864 → Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

d_'8743''45'assoc_244 ∷ T_IsBooleanAlgebra_1864 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8743''45'comm_246 ∷ T_IsBooleanAlgebra_1864 → Bool → Bool → T__'8801'__12 Source #

d_'8743''45'complement'691'_248 ∷ T_IsBooleanAlgebra_1864 → Bool → T__'8801'__12 Source #

d_'8743''45'cong_250 ∷ T_IsBooleanAlgebra_1864 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8744''45'assoc_258 ∷ T_IsBooleanAlgebra_1864 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8744''45'comm_260 ∷ T_IsBooleanAlgebra_1864 → Bool → Bool → T__'8801'__12 Source #

d_'8744''45'complement'691'_262 ∷ T_IsBooleanAlgebra_1864 → Bool → T__'8801'__12 Source #

d_'8744''45'cong_264 ∷ T_IsBooleanAlgebra_1864 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8744''45'distrib'691''45''8743'_270 ∷ T_IsBooleanAlgebra_1864 → Bool → Bool → Bool → T__'8801'__12 Source #

d_assoc_276 ∷ T_IsIdempotentCommutativeMonoid_464 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_278 ∷ T_IsIdempotentCommutativeMonoid_464 → Bool → Bool → T__'8801'__12 Source #

d_idem_280 ∷ T_IsIdempotentCommutativeMonoid_464 → Bool → T__'8801'__12 Source #

d_identity_282 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Σ_14 Source #

d_isCommutativeMonoid_290 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMonoid_406 Source #

d_isEquivalence_294 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsEquivalence_26 Source #

d_isMagma_296 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMagma_86 Source #

d_isMonoid_298 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMonoid_358 Source #

d_isSemigroup_302 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsSemigroup_194 Source #

d_'8729''45'cong_314 ∷ T_IsIdempotentCommutativeMonoid_464 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_322 ∷ T_IsCancellativeCommutativeSemiring_1462 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'42''45'cancel'737''45'nonZero_324 ∷ T_IsCancellativeCommutativeSemiring_1462 → Bool → Bool → Bool → (T__'8801'__12 → T_'8869'_4) → T__'8801'__12 → T__'8801'__12 Source #

d_'42''45'comm_326 ∷ T_IsCancellativeCommutativeSemiring_1462 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_328 ∷ T_IsCancellativeCommutativeSemiring_1462 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_334 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_isMagma_346 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMagma_86 Source #

d_'42''45'isMonoid_348 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMonoid_358 Source #

d_isSemigroup_350 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemigroup_194 Source #

d_assoc_352 ∷ T_IsCancellativeCommutativeSemiring_1462 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_354 ∷ T_IsCancellativeCommutativeSemiring_1462 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_356 ∷ T_IsCancellativeCommutativeSemiring_1462 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_362 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_370 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeMonoid_406 Source #

d_isMagma_374 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMagma_86 Source #

d_isMonoid_376 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsMonoid_358 Source #

d_isSemigroup_378 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemigroup_194 Source #

d_distrib_380 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_isCommutativeSemiring_386 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsCommutativeSemiring_1344 Source #

d_isEquivalence_390 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsEquivalence_26 Source #

d_isNearSemiring_392 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → Bool → T_IsCancellativeCommutativeSemiring_1462 → T_IsNearSemiring_876 Source #

du_isNearSemiring_392 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsNearSemiring_876 Source #

d_isSemiring_396 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiring_1238 Source #

d_isSemiringWithoutAnnihilatingZero_398 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiringWithoutOne_400 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → Bool → T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_400 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_IsSemiringWithoutOne_952 Source #

d_zero_412 ∷ T_IsCancellativeCommutativeSemiring_1462 → T_Σ_14 Source #

d_comm_420 ∷ T_IsCommutativeMagma_122 → Bool → Bool → T__'8801'__12 Source #

d_isEquivalence_422 ∷ T_IsCommutativeMagma_122 → T_IsEquivalence_26 Source #

d_isMagma_424 ∷ T_IsCommutativeMagma_122 → T_IsMagma_86 Source #

d_'8729''45'cong_438 ∷ T_IsCommutativeMagma_122 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_446 ∷ T_IsCommutativeMonoid_406 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_448 ∷ T_IsCommutativeMonoid_406 → Bool → Bool → T__'8801'__12 Source #

d_identity_450 ∷ T_IsCommutativeMonoid_406 → T_Σ_14 Source #

d_isEquivalence_460 ∷ T_IsCommutativeMonoid_406 → T_IsEquivalence_26 Source #

d_isMagma_462 ∷ T_IsCommutativeMonoid_406 → T_IsMagma_86 Source #

d_isMonoid_464 ∷ T_IsCommutativeMonoid_406 → T_IsMonoid_358 Source #

d_isSemigroup_468 ∷ T_IsCommutativeMonoid_406 → T_IsSemigroup_194 Source #

d_'8729''45'cong_480 ∷ T_IsCommutativeMonoid_406 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_490 ∷ T_IsCommutativeRing_1720 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'42''45'comm_492 ∷ T_IsCommutativeRing_1720 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_494 ∷ T_IsCommutativeRing_1720 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_500 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_isMagma_512 ∷ T_IsCommutativeRing_1720 → T_IsMagma_86 Source #

d_'42''45'isMonoid_514 ∷ T_IsCommutativeRing_1720 → T_IsMonoid_358 Source #

d_isSemigroup_516 ∷ T_IsCommutativeRing_1720 → T_IsSemigroup_194 Source #

d_assoc_518 ∷ T_IsCommutativeRing_1720 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_520 ∷ T_IsCommutativeRing_1720 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_522 ∷ T_IsCommutativeRing_1720 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_528 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_'43''45'isAbelianGroup_534 ∷ T_IsCommutativeRing_1720 → T_IsAbelianGroup_662 Source #

d_isGroup_542 ∷ T_IsCommutativeRing_1720 → T_IsGroup_580 Source #

d_isMagma_544 ∷ T_IsCommutativeRing_1720 → T_IsMagma_86 Source #

d_isMonoid_546 ∷ T_IsCommutativeRing_1720 → T_IsMonoid_358 Source #

d_isSemigroup_548 ∷ T_IsCommutativeRing_1720 → T_IsSemigroup_194 Source #

d_'8315''185''45'cong_550 ∷ T_IsCommutativeRing_1720 → Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

d_inverse_552 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_distrib_558 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_isEquivalence_568 ∷ T_IsCommutativeRing_1720 → T_IsEquivalence_26 Source #

d_isNearSemiring_570 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → (Bool → Bool) → Bool → Bool → T_IsCommutativeRing_1720 → T_IsNearSemiring_876 Source #

du_isNearSemiring_570 ∷ T_IsCommutativeRing_1720 → T_IsNearSemiring_876 Source #

d_isRing_574 ∷ T_IsCommutativeRing_1720 → T_IsRing_1584 Source #

d_isSemiring_576 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → (Bool → Bool) → Bool → Bool → T_IsCommutativeRing_1720 → T_IsSemiring_1238 Source #

du_isSemiring_576 ∷ T_IsCommutativeRing_1720 → T_IsSemiring_1238 Source #

d_isSemiringWithoutOne_580 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → (Bool → Bool) → Bool → Bool → T_IsCommutativeRing_1720 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_580 ∷ T_IsCommutativeRing_1720 → T_IsSemiringWithoutOne_952 Source #

d_zero_596 ∷ T_IsCommutativeRing_1720 → T_Σ_14 Source #

d_assoc_604 ∷ T_IsCommutativeSemigroup_270 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_606 ∷ T_IsCommutativeSemigroup_270 → Bool → Bool → T__'8801'__12 Source #

d_isEquivalence_610 ∷ T_IsCommutativeSemigroup_270 → T_IsEquivalence_26 Source #

d_isMagma_612 ∷ T_IsCommutativeSemigroup_270 → T_IsMagma_86 Source #

d_isSemigroup_616 ∷ T_IsCommutativeSemigroup_270 → T_IsSemigroup_194 Source #

d_'8729''45'cong_628 ∷ T_IsCommutativeSemigroup_270 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_636 ∷ T_IsCommutativeSemiring_1344 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'42''45'comm_638 ∷ T_IsCommutativeSemiring_1344 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_640 ∷ T_IsCommutativeSemiring_1344 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_646 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_isMagma_658 ∷ T_IsCommutativeSemiring_1344 → T_IsMagma_86 Source #

d_'42''45'isMonoid_660 ∷ T_IsCommutativeSemiring_1344 → T_IsMonoid_358 Source #

d_isSemigroup_662 ∷ T_IsCommutativeSemiring_1344 → T_IsSemigroup_194 Source #

d_assoc_664 ∷ T_IsCommutativeSemiring_1344 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_666 ∷ T_IsCommutativeSemiring_1344 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_668 ∷ T_IsCommutativeSemiring_1344 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_674 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_682 ∷ T_IsCommutativeSemiring_1344 → T_IsCommutativeMonoid_406 Source #

d_isMagma_686 ∷ T_IsCommutativeSemiring_1344 → T_IsMagma_86 Source #

d_isMonoid_688 ∷ T_IsCommutativeSemiring_1344 → T_IsMonoid_358 Source #

d_isSemigroup_690 ∷ T_IsCommutativeSemiring_1344 → T_IsSemigroup_194 Source #

d_distrib_692 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_isEquivalence_700 ∷ T_IsCommutativeSemiring_1344 → T_IsEquivalence_26 Source #

d_isNearSemiring_702 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → Bool → T_IsCommutativeSemiring_1344 → T_IsNearSemiring_876 Source #

du_isNearSemiring_702 ∷ T_IsCommutativeSemiring_1344 → T_IsNearSemiring_876 Source #

d_isSemiring_706 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiring_1238 Source #

d_isSemiringWithoutAnnihilatingZero_708 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiringWithoutOne_710 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → Bool → T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_710 ∷ T_IsCommutativeSemiring_1344 → T_IsSemiringWithoutOne_952 Source #

d_zero_722 ∷ T_IsCommutativeSemiring_1344 → T_Σ_14 Source #

d_assoc_730 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'42''45'comm_732 ∷ T_IsCommutativeSemiringWithoutOne_1044 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_734 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_isMagma_744 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

du_isMagma_744 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_746 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

d_assoc_748 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_750 ∷ T_IsCommutativeSemiringWithoutOne_1044 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_752 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_758 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

du_identity_758 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_766 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsCommutativeMonoid_406 Source #

d_isMagma_770 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

du_isMagma_770 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMagma_86 Source #

d_isMonoid_772 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsMonoid_358 Source #

d_isSemigroup_774 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

du_isSemigroup_774 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemigroup_194 Source #

d_distrib_776 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

d_distrib'691'_778 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → Bool → Bool → Bool → T__'8801'__12 Source #

d_isEquivalence_780 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → T_IsEquivalence_26 Source #

du_isEquivalence_780 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsEquivalence_26 Source #

d_isNearSemiring_782 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsCommutativeSemiringWithoutOne_1044 → T_IsNearSemiring_876 Source #

du_isNearSemiring_782 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsNearSemiring_876 Source #

d_isSemiringWithoutOne_786 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_IsSemiringWithoutOne_952 Source #

d_zero_798 ∷ T_IsCommutativeSemiringWithoutOne_1044 → T_Σ_14 Source #

d_absorptive_806 ∷ T_IsDistributiveLattice_814 → T_Σ_14 Source #

d_isEquivalence_808 ∷ T_IsDistributiveLattice_814 → T_IsEquivalence_26 Source #

d_isLattice_810 ∷ T_IsDistributiveLattice_814 → T_IsLattice_740 Source #

d_'8743''45'assoc_824 ∷ T_IsDistributiveLattice_814 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8743''45'comm_826 ∷ T_IsDistributiveLattice_814 → Bool → Bool → T__'8801'__12 Source #

d_'8743''45'cong_828 ∷ T_IsDistributiveLattice_814 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8744''45'assoc_836 ∷ T_IsDistributiveLattice_814 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8744''45'comm_838 ∷ T_IsDistributiveLattice_814 → Bool → Bool → T__'8801'__12 Source #

d_'8744''45'cong_840 ∷ T_IsDistributiveLattice_814 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8744''45'distrib'691''45''8743'_846 ∷ T_IsDistributiveLattice_814 → Bool → Bool → Bool → T__'8801'__12 Source #

d_assoc_854 ∷ T_IsGroup_580 → Bool → Bool → Bool → T__'8801'__12 Source #

d_identity_856 ∷ T_IsGroup_580 → T_Σ_14 Source #

d_inverse_862 ∷ T_IsGroup_580 → T_Σ_14 Source #

d_isEquivalence_868 ∷ T_IsGroup_580 → T_IsEquivalence_26 Source #

d_isMagma_870 ∷ T_IsGroup_580 → T_IsMagma_86 Source #

d_isMonoid_872 ∷ T_IsGroup_580 → T_IsMonoid_358 Source #

d_isSemigroup_876 ∷ T_IsGroup_580 → T_IsSemigroup_194 Source #

d_'8315''185''45'cong_892 ∷ T_IsGroup_580 → Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

d_'8729''45'cong_894 ∷ T_IsGroup_580 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_902 ∷ T_IsIdempotentCommutativeMonoid_464 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_904 ∷ T_IsIdempotentCommutativeMonoid_464 → Bool → Bool → T__'8801'__12 Source #

d_idem_906 ∷ T_IsIdempotentCommutativeMonoid_464 → Bool → T__'8801'__12 Source #

d_identity_908 ∷ T_IsIdempotentCommutativeMonoid_464 → T_Σ_14 Source #

d_isCommutativeMonoid_916 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsCommutativeMonoid_406 Source #

d_isEquivalence_920 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsEquivalence_26 Source #

d_isMagma_922 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMagma_86 Source #

d_isMonoid_924 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsMonoid_358 Source #

d_isSemigroup_928 ∷ T_IsIdempotentCommutativeMonoid_464 → T_IsSemigroup_194 Source #

d_'8729''45'cong_940 ∷ T_IsIdempotentCommutativeMonoid_464 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_absorptive_948 ∷ T_IsLattice_740 → T_Σ_14 Source #

d_isEquivalence_950 ∷ T_IsLattice_740 → T_IsEquivalence_26 Source #

d_'8743''45'assoc_964 ∷ T_IsLattice_740 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8743''45'comm_966 ∷ T_IsLattice_740 → Bool → Bool → T__'8801'__12 Source #

d_'8743''45'cong_968 ∷ T_IsLattice_740 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_'8744''45'assoc_976 ∷ T_IsLattice_740 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8744''45'comm_978 ∷ T_IsLattice_740 → Bool → Bool → T__'8801'__12 Source #

d_'8744''45'cong_980 ∷ T_IsLattice_740 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_isEquivalence_988 ∷ T_IsMagma_86 → T_IsEquivalence_26 Source #

d_'8729''45'cong_1002 ∷ T_IsMagma_86 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1010 ∷ T_IsMonoid_358 → Bool → Bool → Bool → T__'8801'__12 Source #

d_identity_1012 ∷ T_IsMonoid_358 → T_Σ_14 Source #

d_isEquivalence_1018 ∷ T_IsMonoid_358 → T_IsEquivalence_26 Source #

d_isMagma_1020 ∷ T_IsMonoid_358 → T_IsMagma_86 Source #

d_isSemigroup_1024 ∷ T_IsMonoid_358 → T_IsSemigroup_194 Source #

d_'8729''45'cong_1036 ∷ T_IsMonoid_358 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1044 ∷ T_IsNearSemiring_876 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1046 ∷ T_IsNearSemiring_876 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_isMagma_1052 ∷ T_IsNearSemiring_876 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_1054 ∷ T_IsNearSemiring_876 → T_IsSemigroup_194 Source #

d_assoc_1056 ∷ T_IsNearSemiring_876 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1058 ∷ T_IsNearSemiring_876 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1064 ∷ T_IsNearSemiring_876 → T_Σ_14 Source #

d_isMagma_1070 ∷ T_IsNearSemiring_876 → T_IsMagma_86 Source #

d_'43''45'isMonoid_1072 ∷ T_IsNearSemiring_876 → T_IsMonoid_358 Source #

d_isSemigroup_1074 ∷ T_IsNearSemiring_876 → T_IsSemigroup_194 Source #

d_distrib'691'_1076 ∷ T_IsNearSemiring_876 → Bool → Bool → Bool → T__'8801'__12 Source #

d_isEquivalence_1078 ∷ T_IsNearSemiring_876 → T_IsEquivalence_26 Source #

d_zero'737'_1092 ∷ T_IsNearSemiring_876 → Bool → T__'8801'__12 Source #

d_assoc_1098 ∷ T_IsRing_1584 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1100 ∷ T_IsRing_1584 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1106 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_isMagma_1112 ∷ T_IsRing_1584 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1114 ∷ T_IsRing_1584 → T_IsMonoid_358 Source #

d_isSemigroup_1116 ∷ T_IsRing_1584 → T_IsSemigroup_194 Source #

d_assoc_1118 ∷ T_IsRing_1584 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_1120 ∷ T_IsRing_1584 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1122 ∷ T_IsRing_1584 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1128 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_'43''45'isAbelianGroup_1134 ∷ T_IsRing_1584 → T_IsAbelianGroup_662 Source #

d_isGroup_1142 ∷ T_IsRing_1584 → T_IsGroup_580 Source #

d_isMagma_1144 ∷ T_IsRing_1584 → T_IsMagma_86 Source #

d_isMonoid_1146 ∷ T_IsRing_1584 → T_IsMonoid_358 Source #

d_isSemigroup_1148 ∷ T_IsRing_1584 → T_IsSemigroup_194 Source #

d_'8315''185''45'cong_1150 ∷ T_IsRing_1584 → Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

d_inverse_1152 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_distrib_1158 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_isEquivalence_1164 ∷ T_IsRing_1584 → T_IsEquivalence_26 Source #

d_isNearSemiring_1166 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → (Bool → Bool) → Bool → Bool → T_IsRing_1584 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1166 ∷ T_IsRing_1584 → T_IsNearSemiring_876 Source #

d_isSemiring_1170 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → (Bool → Bool) → Bool → Bool → T_IsRing_1584 → T_IsSemiring_1238 Source #

d_isSemiringWithoutOne_1174 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → (Bool → Bool) → Bool → Bool → T_IsRing_1584 → T_IsSemiringWithoutOne_952 Source #

du_isSemiringWithoutOne_1174 ∷ T_IsRing_1584 → T_IsSemiringWithoutOne_952 Source #

d_zero_1190 ∷ T_IsRing_1584 → T_Σ_14 Source #

d_isEquivalence_1198 ∷ T_IsSelectiveMagma_158 → T_IsEquivalence_26 Source #

d_isMagma_1200 ∷ T_IsSelectiveMagma_158 → T_IsMagma_86 Source #

d_sel_1208 ∷ T_IsSelectiveMagma_158 → Bool → Bool → T__'8846'__30 Source #

d_'8729''45'cong_1216 ∷ T_IsSelectiveMagma_158 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1224 ∷ T_IsSemigroup_194 → Bool → Bool → Bool → T__'8801'__12 Source #

d_isEquivalence_1226 ∷ T_IsSemigroup_194 → T_IsEquivalence_26 Source #

d_isMagma_1228 ∷ T_IsSemigroup_194 → T_IsMagma_86 Source #

d_'8729''45'cong_1242 ∷ T_IsSemigroup_194 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1250 ∷ T_IsSemilattice_312 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_1252 ∷ T_IsSemilattice_312 → Bool → Bool → T__'8801'__12 Source #

d_idem_1254 ∷ T_IsSemilattice_312 → Bool → T__'8801'__12 Source #

d_isBand_1256 ∷ T_IsSemilattice_312 → T_IsBand_230 Source #

d_isEquivalence_1258 ∷ T_IsSemilattice_312 → T_IsEquivalence_26 Source #

d_isMagma_1260 ∷ T_IsSemilattice_312 → T_IsMagma_86 Source #

d_isSemigroup_1264 ∷ T_IsSemilattice_312 → T_IsSemigroup_194 Source #

d_'8729''45'cong_1276 ∷ T_IsSemilattice_312 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_assoc_1284 ∷ T_IsSemiring_1238 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1286 ∷ T_IsSemiring_1238 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1292 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_isMagma_1298 ∷ T_IsSemiring_1238 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1300 ∷ T_IsSemiring_1238 → T_IsMonoid_358 Source #

d_isSemigroup_1302 ∷ T_IsSemiring_1238 → T_IsSemigroup_194 Source #

d_assoc_1304 ∷ T_IsSemiring_1238 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_1306 ∷ T_IsSemiring_1238 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1308 ∷ T_IsSemiring_1238 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1314 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_1322 ∷ T_IsSemiring_1238 → T_IsCommutativeMonoid_406 Source #

d_isMagma_1326 ∷ T_IsSemiring_1238 → T_IsMagma_86 Source #

d_isMonoid_1328 ∷ T_IsSemiring_1238 → T_IsMonoid_358 Source #

d_isSemigroup_1330 ∷ T_IsSemiring_1238 → T_IsSemigroup_194 Source #

d_distrib_1332 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_isEquivalence_1338 ∷ T_IsSemiring_1238 → T_IsEquivalence_26 Source #

d_isNearSemiring_1340 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → Bool → T_IsSemiring_1238 → T_IsNearSemiring_876 Source #

du_isNearSemiring_1340 ∷ T_IsSemiring_1238 → T_IsNearSemiring_876 Source #

d_isSemiringWithoutAnnihilatingZero_1344 ∷ T_IsSemiring_1238 → T_IsSemiringWithoutAnnihilatingZero_1142 Source #

d_isSemiringWithoutOne_1346 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → Bool → T_IsSemiring_1238 → T_IsSemiringWithoutOne_952 Source #

d_zero_1358 ∷ T_IsSemiring_1238 → T_Σ_14 Source #

d_assoc_1366 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1368 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1374 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_isMagma_1380 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMagma_86 Source #

d_'42''45'isMonoid_1382 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMonoid_358 Source #

d_isSemigroup_1384 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsSemigroup_194 Source #

d_assoc_1386 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_1388 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1390 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1396 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_1404 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsCommutativeMonoid_406 Source #

d_isMagma_1408 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMagma_86 Source #

d_isMonoid_1410 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsMonoid_358 Source #

d_isSemigroup_1412 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsSemigroup_194 Source #

d_distrib_1414 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_Σ_14 Source #

d_isEquivalence_1420 ∷ T_IsSemiringWithoutAnnihilatingZero_1142 → T_IsEquivalence_26 Source #

d_assoc_1436 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → Bool → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1438 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_isMagma_1444 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

du_isMagma_1444 ∷ T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

d_'42''45'isSemigroup_1446 ∷ T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

d_assoc_1448 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → Bool → Bool → Bool → T__'8801'__12 Source #

d_comm_1450 ∷ T_IsSemiringWithoutOne_952 → Bool → Bool → T__'8801'__12 Source #

d_'8729''45'cong_1452 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1458 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

du_identity_1458 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

d_'43''45'isCommutativeMonoid_1466 ∷ T_IsSemiringWithoutOne_952 → T_IsCommutativeMonoid_406 Source #

d_isMagma_1470 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

du_isMagma_1470 ∷ T_IsSemiringWithoutOne_952 → T_IsMagma_86 Source #

d_isMonoid_1472 ∷ T_IsSemiringWithoutOne_952 → T_IsMonoid_358 Source #

d_isSemigroup_1474 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

du_isSemigroup_1474 ∷ T_IsSemiringWithoutOne_952 → T_IsSemigroup_194 Source #

d_distrib_1476 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

d_distrib'691'_1478 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → Bool → Bool → Bool → T__'8801'__12 Source #

d_isEquivalence_1480 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → T_IsEquivalence_26 Source #

du_isEquivalence_1480 ∷ T_IsSemiringWithoutOne_952 → T_IsEquivalence_26 Source #

d_isNearSemiring_1482 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → Bool → T_IsSemiringWithoutOne_952 → T_IsNearSemiring_876 Source #

d_zero_1496 ∷ T_IsSemiringWithoutOne_952 → T_Σ_14 Source #

d__'8799'__1510 ∷ Bool → Bool → T_Dec_32 Source #

d_'8801''45'setoid_1512 ∷ T_Setoid_44 Source #

d_'8801''45'decSetoid_1514 ∷ T_DecSetoid_84 Source #

d_'8804''45'reflexive_1516 ∷ Bool → Bool → T__'8801'__12 → T__'8804'__10 Source #

du_'8804''45'reflexive_1516 ∷ T__'8804'__10 Source #

d_'8804''45'refl_1518 ∷ Bool → T__'8804'__10 Source #

du_'8804''45'refl_1518 ∷ T__'8804'__10 Source #

d_'8804''45'trans_1520 ∷ Bool → Bool → Bool → T__'8804'__10 → T__'8804'__10 → T__'8804'__10 Source #

du_'8804''45'trans_1520 ∷ T__'8804'__10 → T__'8804'__10 → T__'8804'__10 Source #

d_'8804''45'antisym_1524 ∷ Bool → Bool → T__'8804'__10 → T__'8804'__10 → T__'8801'__12 Source #

d_'8804''45'minimum_1526 ∷ Bool → T__'8804'__10 Source #

d_'8804''45'maximum_1528 ∷ Bool → T__'8804'__10 Source #

d_'8804''45'total_1530 ∷ Bool → Bool → T__'8846'__30 Source #

d__'8804''63'__1536 ∷ Bool → Bool → T_Dec_32 Source #

d_'8804''45'irrelevant_1540 ∷ Bool → Bool → T__'8804'__10 → T__'8804'__10 → T__'8801'__12 Source #

d_'8804''45'isPreorder_1542 ∷ T_IsPreorder_70 Source #

d_'8804''45'isPartialOrder_1544 ∷ T_IsPartialOrder_162 Source #

d_'8804''45'isTotalOrder_1546 ∷ T_IsTotalOrder_384 Source #

d_'8804''45'isDecTotalOrder_1548 ∷ T_IsDecTotalOrder_434 Source #

d_'8804''45'poset_1550 ∷ T_Poset_282 Source #

d_'8804''45'preorder_1552 ∷ T_Preorder_132 Source #

d_'8804''45'totalOrder_1554 ∷ T_TotalOrder_652 Source #

d_'8804''45'decTotalOrder_1556 ∷ T_DecTotalOrder_740 Source #

d_'60''45'irrefl_1558 ∷ Bool → Bool → T__'8801'__12 → T__'60'__18 → T_'8869'_4 Source #

d_'60''45'asym_1560 ∷ Bool → Bool → T__'60'__18 → T__'60'__18 → T_'8869'_4 Source #

d_'60''45'trans_1562 ∷ Bool → Bool → Bool → T__'60'__18 → T__'60'__18 → T__'60'__18 Source #

d_'60''45'trans'691'_1564 ∷ Bool → Bool → Bool → T__'8804'__10 → T__'60'__18 → T__'60'__18 Source #

d_'60''45'trans'737'_1566 ∷ Bool → Bool → Bool → T__'60'__18 → T__'8804'__10 → T__'60'__18 Source #

d_'60''45'cmp_1568 ∷ Bool → Bool → T_Tri_136 Source #

d__'60''63'__1570 ∷ Bool → Bool → T_Dec_32 Source #

d_'60''45'resp'8322''45''8801'_1572 ∷ T_Σ_14 Source #

d_'60''45'irrelevant_1578 ∷ Bool → Bool → T__'60'__18 → T__'60'__18 → T__'8801'__12 Source #

d_'60''45'isStrictPartialOrder_1580 ∷ T_IsStrictPartialOrder_266 Source #

d_'60''45'isStrictTotalOrder_1582 ∷ T_IsStrictTotalOrder_502 Source #

d_'60''45'strictPartialOrder_1584 ∷ T_StrictPartialOrder_472 Source #

d_'60''45'strictTotalOrder_1586 ∷ T_StrictTotalOrder_864 Source #

d_'8744''45'assoc_1588 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_'8744''45'comm_1598 ∷ Bool → Bool → T__'8801'__12 Source #

d_'8744''45'identity'737'_1600 ∷ Bool → T__'8801'__12 Source #

d_'8744''45'identity'691'_1602 ∷ Bool → T__'8801'__12 Source #

d_'8744''45'identity_1604 ∷ T_Σ_14 Source #

d_'8744''45'zero'737'_1606 ∷ Bool → T__'8801'__12 Source #

d_'8744''45'zero'691'_1608 ∷ Bool → T__'8801'__12 Source #

d_'8744''45'zero_1610 ∷ T_Σ_14 Source #

d_'8744''45'inverse'737'_1612 ∷ Bool → T__'8801'__12 Source #

d_'8744''45'inverse'691'_1614 ∷ Bool → T__'8801'__12 Source #

d_'8744''45'inverse_1618 ∷ T_Σ_14 Source #

d_'8744''45'idem_1620 ∷ Bool → T__'8801'__12 Source #

d_'8744''45'sel_1622 ∷ Bool → Bool → T__'8846'__30 Source #

du_'8744''45'sel_1622 ∷ Bool → T__'8846'__30 Source #

d_'8744''45'isMagma_1628 ∷ T_IsMagma_86 Source #

d_'8744''45'magma_1630 ∷ T_Magma_36 Source #

d_'8744''45'isSemigroup_1632 ∷ T_IsSemigroup_194 Source #

d_'8744''45'semigroup_1634 ∷ T_Semigroup_206 Source #

d_'8744''45'isBand_1636 ∷ T_IsBand_230 Source #

d_'8744''45'band_1638 ∷ T_Band_266 Source #

d_'8744''45'isSemilattice_1640 ∷ T_IsSemilattice_312 Source #

d_'8744''45'semilattice_1642 ∷ T_Semilattice_402 Source #

d_'8744''45'isMonoid_1644 ∷ T_IsMonoid_358 Source #

d_'8744''45'isCommutativeMonoid_1646 ∷ T_IsCommutativeMonoid_406 Source #

d_'8744''45'commutativeMonoid_1648 ∷ T_CommutativeMonoid_582 Source #

d_'8744''45'isIdempotentCommutativeMonoid_1650 ∷ T_IsIdempotentCommutativeMonoid_464 Source #

d_'8744''45'idempotentCommutativeMonoid_1652 ∷ T_IdempotentCommutativeMonoid_674 Source #

d_'8743''45'assoc_1654 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_'8743''45'comm_1664 ∷ Bool → Bool → T__'8801'__12 Source #

d_'8743''45'identity'737'_1666 ∷ Bool → T__'8801'__12 Source #

d_'8743''45'identity'691'_1668 ∷ Bool → T__'8801'__12 Source #

d_'8743''45'identity_1670 ∷ T_Σ_14 Source #

d_'8743''45'zero'737'_1672 ∷ Bool → T__'8801'__12 Source #

d_'8743''45'zero'691'_1674 ∷ Bool → T__'8801'__12 Source #

d_'8743''45'zero_1676 ∷ T_Σ_14 Source #

d_'8743''45'inverse'737'_1678 ∷ Bool → T__'8801'__12 Source #

d_'8743''45'inverse'691'_1680 ∷ Bool → T__'8801'__12 Source #

d_'8743''45'inverse_1684 ∷ T_Σ_14 Source #

d_'8743''45'idem_1686 ∷ Bool → T__'8801'__12 Source #

d_'8743''45'sel_1688 ∷ Bool → Bool → T__'8846'__30 Source #

du_'8743''45'sel_1688 ∷ Bool → T__'8846'__30 Source #

d_'8743''45'distrib'737''45''8744'_1694 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_'8743''45'distrib'691''45''8744'_1704 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_'8743''45'distrib'45''8744'_1712 ∷ T_Σ_14 Source #

d_'8744''45'distrib'737''45''8743'_1714 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_'8744''45'distrib'691''45''8743'_1724 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_'8744''45'distrib'45''8743'_1732 ∷ T_Σ_14 Source #

d_'8743''45'abs'45''8744'_1734 ∷ Bool → Bool → T__'8801'__12 Source #

d_'8744''45'abs'45''8743'_1740 ∷ Bool → Bool → T__'8801'__12 Source #

d_'8744''45''8743''45'absorptive_1746 ∷ T_Σ_14 Source #

d_'8743''45'isMagma_1748 ∷ T_IsMagma_86 Source #

d_'8743''45'magma_1750 ∷ T_Magma_36 Source #

d_'8743''45'isSemigroup_1752 ∷ T_IsSemigroup_194 Source #

d_'8743''45'semigroup_1754 ∷ T_Semigroup_206 Source #

d_'8743''45'isBand_1756 ∷ T_IsBand_230 Source #

d_'8743''45'band_1758 ∷ T_Band_266 Source #

d_'8743''45'isSemilattice_1760 ∷ T_IsSemilattice_312 Source #

d_'8743''45'semilattice_1762 ∷ T_Semilattice_402 Source #

d_'8743''45'isMonoid_1764 ∷ T_IsMonoid_358 Source #

d_'8743''45'isCommutativeMonoid_1766 ∷ T_IsCommutativeMonoid_406 Source #

d_'8743''45'commutativeMonoid_1768 ∷ T_CommutativeMonoid_582 Source #

d_'8743''45'isIdempotentCommutativeMonoid_1770 ∷ T_IsIdempotentCommutativeMonoid_464 Source #

d_'8743''45'idempotentCommutativeMonoid_1772 ∷ T_IdempotentCommutativeMonoid_674 Source #

d_'8744''45''8743''45'isSemiring_1774 ∷ T_IsSemiring_1238 Source #

d_'8744''45''8743''45'isCommutativeSemiring_1776 ∷ T_IsCommutativeSemiring_1344 Source #

d_'8744''45''8743''45'commutativeSemiring_1778 ∷ T_CommutativeSemiring_2094 Source #

d_'8743''45''8744''45'isSemiring_1780 ∷ T_IsSemiring_1238 Source #

d_'8743''45''8744''45'isCommutativeSemiring_1782 ∷ T_IsCommutativeSemiring_1344 Source #

d_'8743''45''8744''45'commutativeSemiring_1784 ∷ T_CommutativeSemiring_2094 Source #

d_'8744''45''8743''45'isLattice_1786 ∷ T_IsLattice_740 Source #

d_'8744''45''8743''45'lattice_1788 ∷ T_Lattice_1144 Source #

d_'8744''45''8743''45'isDistributiveLattice_1790 ∷ T_IsDistributiveLattice_814 Source #

d_'8744''45''8743''45'distributiveLattice_1792 ∷ T_DistributiveLattice_1228 Source #

d_'8744''45''8743''45'isBooleanAlgebra_1794 ∷ T_IsBooleanAlgebra_1864 Source #

d_'8744''45''8743''45'booleanAlgebra_1796 ∷ T_BooleanAlgebra_2920 Source #

d_xor'45'is'45'ok_1802 ∷ Bool → Bool → T__'8801'__12 Source #

d_xor'45''8743''45'commutativeRing_1808 ∷ T_CommutativeRing_2704 Source #

d_not'45'involutive_2140 ∷ Bool → T__'8801'__12 Source #

d_not'45'injective_2146 ∷ Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

d_not'45''172'_2156 ∷ Bool → Bool → T__'8801'__12 → T__'8801'__12 → T_'8869'_4 Source #

d_'172''45'not_2162 ∷ Bool → Bool → (T__'8801'__12 → T_'8869'_4) → T__'8801'__12 Source #

d_'8660''8594''8801'_2174 ∷ Bool → Bool → Bool → T_Equivalence_16 → T__'8801'__12 Source #

d_T'45''8801'_2190 ∷ Bool → T_Equivalence_16 Source #

d_T'45'not'45''8801'_2194 ∷ Bool → T_Equivalence_16 Source #

d_T'45''8743'_2200 ∷ Bool → Bool → T_Equivalence_16 Source #

d_T'45''8744'_2206 ∷ Bool → Bool → T_Equivalence_16 Source #

d_T'45'irrelevant_2208 ∷ Bool → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_T'63'_2210 ∷ Bool → T_Dec_32 Source #

d_T'63''45'diag_2216 ∷ Bool → AgdaAny → AgdaAny Source #

du_T'63''45'diag_2216 ∷ Bool → AgdaAny Source #

d_push'45'function'45'into'45'if_2226 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Bool → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_'8743''45''8744''45'dist'737'_2228 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_'8743''45''8744''45'dist'691'_2230 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_distrib'45''8743''45''8744'_2232 ∷ T_Σ_14 Source #

d_'8744''45''8743''45'dist'737'_2234 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_'8744''45''8743''45'dist'691'_2236 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_'8744''45''8743''45'distrib_2238 ∷ T_Σ_14 Source #

d_'8744''45''8743''45'abs_2240 ∷ Bool → Bool → T__'8801'__12 Source #

d_'8743''45''8744''45'abs_2242 ∷ Bool → Bool → T__'8801'__12 Source #

d_not'45''8743''45'inverse'737'_2244 ∷ Bool → T__'8801'__12 Source #

d_not'45''8743''45'inverse'691'_2246 ∷ Bool → T__'8801'__12 Source #

d_not'45''8743''45'inverse_2248 ∷ T_Σ_14 Source #

d_not'45''8744''45'inverse'737'_2250 ∷ Bool → T__'8801'__12 Source #

d_not'45''8744''45'inverse'691'_2252 ∷ Bool → T__'8801'__12 Source #

d_not'45''8744''45'inverse_2254 ∷ T_Σ_14 Source #

d_isCommutativeSemiring'45''8744''45''8743'_2256 ∷ T_IsCommutativeSemiring_1344 Source #

d_commutativeSemiring'45''8744''45''8743'_2258 ∷ T_CommutativeSemiring_2094 Source #

d_isCommutativeSemiring'45''8743''45''8744'_2260 ∷ T_IsCommutativeSemiring_1344 Source #

d_commutativeSemiring'45''8743''45''8744'_2262 ∷ T_CommutativeSemiring_2094 Source #

d_isBooleanAlgebra_2264 ∷ T_IsBooleanAlgebra_1864 Source #

d_booleanAlgebra_2266 ∷ T_BooleanAlgebra_2920 Source #

d_commutativeRing'45'xor'45''8743'_2268 ∷ T_CommutativeRing_2704 Source #

d_proof'45'irrelevance_2270 ∷ Bool → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_T'45'irrelevance_2272 ∷ Bool → AgdaAny → AgdaAny → T__'8801'__12 Source #