Documentation

d__Absorbs__8 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> () #

d__DistributesOver__10 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> () #

d__DistributesOver'691'__12 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> () #

d__DistributesOver'737'__14 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> () #

d_Absorptive_20 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> () #

d_Associative_30 :: (Bool -> Bool -> Bool) -> () #

d_Commutative_34 :: (Bool -> Bool -> Bool) -> () #

d_Conical_40 :: Bool -> (Bool -> Bool -> Bool) -> () #

d_Idempotent_44 :: (Bool -> Bool -> Bool) -> () #

d_Identity_50 :: Bool -> (Bool -> Bool -> Bool) -> () #

d_Inverse_54 :: Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> () #

d_Involutive_58 :: (Bool -> Bool) -> () #

d_LeftConical_68 :: Bool -> (Bool -> Bool -> Bool) -> () #

d_LeftIdentity_76 :: Bool -> (Bool -> Bool -> Bool) -> () #

d_LeftInverse_78 :: Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> () #

d_LeftZero_84 :: Bool -> (Bool -> Bool -> Bool) -> () #

d_RightConical_98 :: Bool -> (Bool -> Bool -> Bool) -> () #

d_RightIdentity_106 :: Bool -> (Bool -> Bool -> Bool) -> () #

d_RightInverse_108 :: Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> () #

d_RightZero_114 :: Bool -> (Bool -> Bool -> Bool) -> () #

d_Selective_116 :: (Bool -> Bool -> Bool) -> () #

d_Zero_134 :: Bool -> (Bool -> Bool -> Bool) -> () #

d_IsBand_142 :: p -> () #

d_IsCommutativeMonoid_150 :: p -> p -> () #

d_IsCommutativeSemiring_156 :: p -> p -> p -> p -> () #

d_IsIdempotentCommutativeMonoid_164 :: p -> p -> () #

d_IsMagma_182 :: p -> () #

d_IsMonoid_188 :: p -> p -> () #

d_IsSemigroup_210 :: p -> () #

d_IsSemiring_214 :: p -> p -> p -> p -> () #

d_idem_324 :: T_IsBand_508 -> Bool -> T__'8801'__12 #

d_isSemigroup_332 :: T_IsBand_508 -> T_IsSemigroup_472 #

d_comm_520 :: T_IsCommutativeMonoid_736 -> Bool -> Bool -> T__'8801'__12 #

d_isMonoid_536 :: T_IsCommutativeMonoid_736 -> T_IsMonoid_686 #

d_'42''45'comm_720 :: T_IsCommutativeSemiring_1678 -> Bool -> Bool -> T__'8801'__12 #

d_isSemiring_790 :: T_IsCommutativeSemiring_1678 -> T_IsSemiring_1570 #

d_idem_968 :: T_IsIdempotentCommutativeMonoid_852 -> Bool -> T__'8801'__12 #

d_isCommutativeMonoid_982 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMonoid_736 #

d_isEquivalence_1482 :: T_IsMagma_176 -> T_IsEquivalence_26 #

d_'8729''45'cong_1496 :: T_IsMagma_176 -> Bool -> Bool -> Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_identity_1592 :: T_IsMonoid_686 -> T_Σ_14 #

d_isSemigroup_1604 :: T_IsMonoid_686 -> T_IsSemigroup_472 #

d_assoc_2336 :: T_IsSemigroup_472 -> Bool -> Bool -> Bool -> T__'8801'__12 #

d_isMagma_2340 :: T_IsSemigroup_472 -> T_IsMagma_176 #

d_isSemiringWithoutAnnihilatingZero_2454 :: T_IsSemiring_1570 -> T_IsSemiringWithoutAnnihilatingZero_1468 #

d_zero_2468 :: T_IsSemiring_1570 -> T_Σ_14 #

d_IsBooleanAlgebra_2652 :: p -> p -> p -> p -> p -> () #

d_IsDistributiveLattice_2660 :: p -> p -> () #

d_IsLattice_2664 :: p -> p -> () #

d_IsSemilattice_2668 :: (Bool -> Bool -> Bool) -> () #

d_isDistributiveLattice_2674 :: T_IsBooleanAlgebra_3112 -> T_IsDistributiveLattice_3036 #

d_'172''45'cong_2690 :: T_IsBooleanAlgebra_3112 -> Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 #

d_'8743''45'complement_2698 :: T_IsBooleanAlgebra_3112 -> T_Σ_14 #

d_'8744''45'complement_2722 :: T_IsBooleanAlgebra_3112 -> T_Σ_14 #

d_isLattice_2884 :: T_IsDistributiveLattice_3036 -> T_IsLattice_2962 #

d_'8743''45'distrib'45''8744'_2908 :: T_IsDistributiveLattice_3036 -> T_Σ_14 #

d_'8744''45'distrib'45''8743'_2926 :: T_IsDistributiveLattice_3036 -> T_Σ_14 #

d_absorptive_2968 :: T_IsLattice_2962 -> T_Σ_14 #

d_isEquivalence_2970 :: T_IsLattice_2962 -> T_IsEquivalence_26 #

d_'8743''45'assoc_2984 :: T_IsLattice_2962 -> Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8743''45'comm_2986 :: T_IsLattice_2962 -> Bool -> Bool -> T__'8801'__12 #

d_'8743''45'cong_2988 :: T_IsLattice_2962 -> Bool -> Bool -> Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d_'8744''45'assoc_2996 :: T_IsLattice_2962 -> Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8744''45'comm_2998 :: T_IsLattice_2962 -> Bool -> Bool -> T__'8801'__12 #

d_'8744''45'cong_3000 :: T_IsLattice_2962 -> Bool -> Bool -> Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 #

d__'8799'__3082 :: Bool -> Bool -> T_Dec_20 #

d_'8801''45'setoid_3084 :: T_Setoid_44 #

d_'8801''45'decSetoid_3086 :: T_DecSetoid_84 #

d_'8804''45'reflexive_3088 :: Bool -> Bool -> T__'8801'__12 -> T__'8804'__10 #

du_'8804''45'reflexive_3088 :: T__'8804'__10 #

d_'8804''45'refl_3090 :: Bool -> T__'8804'__10 #

du_'8804''45'refl_3090 :: T__'8804'__10 #

d_'8804''45'trans_3092 :: Bool -> Bool -> Bool -> T__'8804'__10 -> T__'8804'__10 -> T__'8804'__10 #

du_'8804''45'trans_3092 :: T__'8804'__10 -> T__'8804'__10 -> T__'8804'__10 #

d_'8804''45'antisym_3096 :: Bool -> Bool -> T__'8804'__10 -> T__'8804'__10 -> T__'8801'__12 #

d_'8804''45'minimum_3098 :: Bool -> T__'8804'__10 #

d_'8804''45'maximum_3100 :: Bool -> T__'8804'__10 #

d_'8804''45'total_3102 :: Bool -> Bool -> T__'8846'__30 #

d__'8804''63'__3108 :: Bool -> Bool -> T_Dec_20 #

d_'8804''45'irrelevant_3112 :: Bool -> Bool -> T__'8804'__10 -> T__'8804'__10 -> T__'8801'__12 #

d_'8804''45'isPreorder_3114 :: T_IsPreorder_70 #

d_'8804''45'isPartialOrder_3116 :: T_IsPartialOrder_174 #

d_'8804''45'isTotalOrder_3118 :: T_IsTotalOrder_404 #

d_'8804''45'isDecTotalOrder_3120 :: T_IsDecTotalOrder_460 #

d_'8804''45'poset_3122 :: T_Poset_314 #

d_'8804''45'preorder_3124 :: T_Preorder_132 #

d_'8804''45'totalOrder_3126 :: T_TotalOrder_764 #

d_'8804''45'decTotalOrder_3128 :: T_DecTotalOrder_866 #

d_'60''45'irrefl_3130 :: Bool -> Bool -> T__'8801'__12 -> T__'60'__18 -> T_Irrelevant_20 #

d_'60''45'asym_3132 :: Bool -> Bool -> T__'60'__18 -> T__'60'__18 -> T_Irrelevant_20 #

d_'60''45'trans_3134 :: Bool -> Bool -> Bool -> T__'60'__18 -> T__'60'__18 -> T__'60'__18 #

d_'60''45'trans'691'_3136 :: Bool -> Bool -> Bool -> T__'8804'__10 -> T__'60'__18 -> T__'60'__18 #

d_'60''45'trans'737'_3138 :: Bool -> Bool -> Bool -> T__'60'__18 -> T__'8804'__10 -> T__'60'__18 #

d_'60''45'cmp_3140 :: Bool -> Bool -> T_Tri_158 #

d__'60''63'__3142 :: Bool -> Bool -> T_Dec_20 #

d_'60''45'resp'8322''45''8801'_3144 :: T_Σ_14 #

d_'60''45'irrelevant_3150 :: Bool -> Bool -> T__'60'__18 -> T__'60'__18 -> T__'8801'__12 #

d_'60''45'wellFounded_3152 :: Bool -> T_Acc_42 #

d_'60''45'acc_3162 :: Bool -> Bool -> Bool -> T__'60'__18 -> T_Acc_42 #

d_'60''45'isStrictPartialOrder_3164 :: T_IsStrictPartialOrder_290 #

d_'60''45'isStrictTotalOrder_3166 :: T_IsStrictTotalOrder_534 #

d_'60''45'strictPartialOrder_3168 :: T_StrictPartialOrder_556 #

d_'60''45'strictTotalOrder_3170 :: T_StrictTotalOrder_1036 #

d_'8744''45'assoc_3172 :: Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8744''45'comm_3182 :: Bool -> Bool -> T__'8801'__12 #

d_'8744''45'identity'737'_3184 :: Bool -> T__'8801'__12 #

d_'8744''45'identity'691'_3186 :: Bool -> T__'8801'__12 #

d_'8744''45'identity_3188 :: T_Σ_14 #

d_'8744''45'zero'737'_3190 :: Bool -> T__'8801'__12 #

d_'8744''45'zero'691'_3192 :: Bool -> T__'8801'__12 #

d_'8744''45'zero_3194 :: T_Σ_14 #

d_'8744''45'inverse'737'_3196 :: Bool -> T__'8801'__12 #

d_'8744''45'inverse'691'_3198 :: Bool -> T__'8801'__12 #

d_'8744''45'inverse_3202 :: T_Σ_14 #

d_'8744''45'idem_3204 :: Bool -> T__'8801'__12 #

d_'8744''45'sel_3206 :: Bool -> Bool -> T__'8846'__30 #

du_'8744''45'sel_3206 :: Bool -> T__'8846'__30 #

d_'8744''45'conical'737'_3212 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 #

d_'8744''45'conical'691'_3214 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 #

d_'8744''45'conical_3216 :: T_Σ_14 #

d_'8744''45'isMagma_3218 :: T_IsMagma_176 #

d_'8744''45'magma_3220 :: T_Magma_68 #

d_'8744''45'isSemigroup_3222 :: T_IsSemigroup_472 #

d_'8744''45'semigroup_3224 :: T_Semigroup_536 #

d_'8744''45'isBand_3226 :: T_IsBand_508 #

d_'8744''45'band_3228 :: T_Band_596 #

d_'8744''45'isSemilattice_3230 :: T_IsCommutativeBand_590 #

d_'8744''45'semilattice_3232 :: T_Semilattice_10 #

d_'8744''45'isMonoid_3234 :: T_IsMonoid_686 #

d_'8744''45'isCommutativeMonoid_3236 :: T_IsCommutativeMonoid_736 #

d_'8744''45'commutativeMonoid_3238 :: T_CommutativeMonoid_962 #

d_'8744''45'isIdempotentCommutativeMonoid_3240 :: T_IsIdempotentCommutativeMonoid_852 #

d_'8744''45'idempotentCommutativeMonoid_3242 :: T_IdempotentCommutativeMonoid_1148 #

d_'8743''45'assoc_3244 :: Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8743''45'comm_3254 :: Bool -> Bool -> T__'8801'__12 #

d_'8743''45'identity'737'_3256 :: Bool -> T__'8801'__12 #

d_'8743''45'identity'691'_3258 :: Bool -> T__'8801'__12 #

d_'8743''45'identity_3260 :: T_Σ_14 #

d_'8743''45'zero'737'_3262 :: Bool -> T__'8801'__12 #

d_'8743''45'zero'691'_3264 :: Bool -> T__'8801'__12 #

d_'8743''45'zero_3266 :: T_Σ_14 #

d_'8743''45'inverse'737'_3268 :: Bool -> T__'8801'__12 #

d_'8743''45'inverse'691'_3270 :: Bool -> T__'8801'__12 #

d_'8743''45'inverse_3274 :: T_Σ_14 #

d_'8743''45'idem_3276 :: Bool -> T__'8801'__12 #

d_'8743''45'sel_3278 :: Bool -> Bool -> T__'8846'__30 #

du_'8743''45'sel_3278 :: Bool -> T__'8846'__30 #

d_'8743''45'conical'737'_3284 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 #

d_'8743''45'conical'691'_3286 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 #

d_'8743''45'conical_3288 :: T_Σ_14 #

d_'8743''45'distrib'737''45''8744'_3290 :: Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8743''45'distrib'691''45''8744'_3300 :: Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8743''45'distrib'45''8744'_3308 :: T_Σ_14 #

d_'8744''45'distrib'737''45''8743'_3310 :: Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8744''45'distrib'691''45''8743'_3320 :: Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8744''45'distrib'45''8743'_3328 :: T_Σ_14 #

d_'8743''45'abs'45''8744'_3330 :: Bool -> Bool -> T__'8801'__12 #

d_'8744''45'abs'45''8743'_3336 :: Bool -> Bool -> T__'8801'__12 #

d_'8744''45''8743''45'absorptive_3342 :: T_Σ_14 #

d_'8743''45'isMagma_3344 :: T_IsMagma_176 #

d_'8743''45'magma_3346 :: T_Magma_68 #

d_'8743''45'isSemigroup_3348 :: T_IsSemigroup_472 #

d_'8743''45'semigroup_3350 :: T_Semigroup_536 #

d_'8743''45'isBand_3352 :: T_IsBand_508 #

d_'8743''45'band_3354 :: T_Band_596 #

d_'8743''45'isSemilattice_3356 :: T_IsCommutativeBand_590 #

d_'8743''45'semilattice_3358 :: T_Semilattice_10 #

d_'8743''45'isMonoid_3360 :: T_IsMonoid_686 #

d_'8743''45'isCommutativeMonoid_3362 :: T_IsCommutativeMonoid_736 #

d_'8743''45'commutativeMonoid_3364 :: T_CommutativeMonoid_962 #

d_'8743''45'isIdempotentCommutativeMonoid_3366 :: T_IsIdempotentCommutativeMonoid_852 #

d_'8743''45'idempotentCommutativeMonoid_3368 :: T_IdempotentCommutativeMonoid_1148 #

d_'8744''45''8743''45'isSemiring_3370 :: T_IsSemiring_1570 #

d_'8744''45''8743''45'isCommutativeSemiring_3372 :: T_IsCommutativeSemiring_1678 #

d_'8744''45''8743''45'commutativeSemiring_3374 :: T_CommutativeSemiring_2446 #

d_'8743''45''8744''45'isSemiring_3376 :: T_IsSemiring_1570 #

d_'8743''45''8744''45'isCommutativeSemiring_3378 :: T_IsCommutativeSemiring_1678 #

d_'8743''45''8744''45'commutativeSemiring_3380 :: T_CommutativeSemiring_2446 #

d_'8744''45''8743''45'isLattice_3382 :: T_IsLattice_2962 #

d_'8744''45''8743''45'lattice_3384 :: T_Lattice_500 #

d_'8744''45''8743''45'isDistributiveLattice_3386 :: T_IsDistributiveLattice_3036 #

d_'8744''45''8743''45'distributiveLattice_3388 :: T_DistributiveLattice_584 #

d_'8744''45''8743''45'isBooleanAlgebra_3390 :: T_IsBooleanAlgebra_3112 #

d_'8744''45''8743''45'booleanAlgebra_3392 :: T_BooleanAlgebra_682 #

d_not'45'involutive_3394 :: Bool -> T__'8801'__12 #

d_not'45'injective_3400 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 #

d_not'45''172'_3410 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 -> T_Irrelevant_20 #

d_'172''45'not_3416 :: Bool -> Bool -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8801'__12 #

d_xor'45'is'45'ok_3426 :: Bool -> Bool -> T__'8801'__12 #

d_true'45'xor_3434 :: Bool -> T__'8801'__12 #

d_xor'45'same_3438 :: Bool -> T__'8801'__12 #

d_not'45'distrib'737''45'xor_3444 :: Bool -> Bool -> T__'8801'__12 #

d_not'45'distrib'691''45'xor_3454 :: Bool -> Bool -> T__'8801'__12 #

d_xor'45'assoc_3460 :: Bool -> Bool -> Bool -> T__'8801'__12 #

d_xor'45'comm_3470 :: Bool -> Bool -> T__'8801'__12 #

d_xor'45'identity'737'_3472 :: Bool -> T__'8801'__12 #

d_xor'45'identity'691'_3474 :: Bool -> T__'8801'__12 #

d_xor'45'identity_3476 :: T_Σ_14 #

d_xor'45'inverse'737'_3478 :: Bool -> T__'8801'__12 #

d_xor'45'inverse'691'_3480 :: Bool -> T__'8801'__12 #

d_xor'45'inverse_3484 :: T_Σ_14 #

d_'8743''45'distrib'737''45'xor_3486 :: Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8743''45'distrib'691''45'xor_3496 :: Bool -> Bool -> Bool -> T__'8801'__12 #

d_'8743''45'distrib'45'xor_3506 :: T_Σ_14 #

d_xor'45'annihilates'45'not_3512 :: Bool -> Bool -> T__'8801'__12 #

d_xor'45''8743''45'commutativeRing_3518 :: T_CommutativeRing_4016 #

d_if'45'float_3792 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> Bool -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_T'45''8801'_3796 :: Bool -> T_Equivalence_1714 #

d_T'45'not'45''8801'_3800 :: Bool -> T_Equivalence_1714 #

d_T'45''8743'_3806 :: Bool -> Bool -> T_Equivalence_1714 #

d_T'45''8744'_3812 :: Bool -> Bool -> T_Equivalence_1714 #

d_T'45'irrelevant_3814 :: Bool -> AgdaAny -> AgdaAny -> T__'8801'__12 #

d_T'63''45'diag_3818 :: Bool -> AgdaAny -> AgdaAny #

d_'8660''8594''8801'_3828 :: Bool -> Bool -> Bool -> T_Equivalence_1714 -> T__'8801'__12 #

d_push'45'function'45'into'45'if_3842 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> Bool -> AgdaAny -> AgdaAny -> T__'8801'__12 #