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_Absorptive_20 ∷ (Bool → Bool → Bool) → (Bool → Bool → Bool) → () Source #

d_Associative_30 ∷ (Bool → Bool → Bool) → () Source #

d_Commutative_34 ∷ (Bool → Bool → Bool) → () Source #

d_Conical_40 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_Idempotent_44 ∷ (Bool → Bool → Bool) → () Source #

d_Identity_50 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_Inverse_54 ∷ Bool → (Bool → Bool) → (Bool → Bool → Bool) → () Source #

d_Involutive_58 ∷ (Bool → Bool) → () Source #

d_LeftConical_68 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_LeftIdentity_76 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_LeftInverse_78 ∷ Bool → (Bool → Bool) → (Bool → Bool → Bool) → () Source #

d_LeftZero_84 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_RightConical_98 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_RightIdentity_106 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_RightInverse_108 ∷ Bool → (Bool → Bool) → (Bool → Bool → Bool) → () Source #

d_RightZero_114 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_Selective_116 ∷ (Bool → Bool → Bool) → () Source #

d_Zero_134 ∷ Bool → (Bool → Bool → Bool) → () Source #

d_IsBand_142 ∷ p → () Source #

d_IsCommutativeMonoid_150 ∷ p → p → () Source #

d_IsCommutativeSemiring_156 ∷ p → p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_164 ∷ p → p → () Source #

d_IsMagma_182 ∷ p → () Source #

d_IsMonoid_188 ∷ p → p → () Source #

d_IsSemigroup_210 ∷ p → () Source #

d_IsSemiring_214 ∷ p → p → p → p → () Source #

d_idem_324 ∷ T_IsBand_508 → Bool → T__'8801'__12 Source #

d_isSemigroup_332 ∷ T_IsBand_508 → T_IsSemigroup_472 Source #

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

d_isMonoid_536 ∷ T_IsCommutativeMonoid_736 → T_IsMonoid_686 Source #

d_'42''45'comm_720 ∷ T_IsCommutativeSemiring_1678 → Bool → Bool → T__'8801'__12 Source #

d_isSemiring_790 ∷ T_IsCommutativeSemiring_1678 → T_IsSemiring_1570 Source #

d_idem_968 ∷ T_IsIdempotentCommutativeMonoid_852 → Bool → T__'8801'__12 Source #

d_isCommutativeMonoid_982 ∷ T_IsIdempotentCommutativeMonoid_852 → T_IsCommutativeMonoid_736 Source #

d_isEquivalence_1482 ∷ T_IsMagma_176 → T_IsEquivalence_26 Source #

d_'8729''45'cong_1496 ∷ T_IsMagma_176 → Bool → Bool → Bool → Bool → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #

d_identity_1592 ∷ T_IsMonoid_686 → T_Σ_14 Source #

d_isSemigroup_1604 ∷ T_IsMonoid_686 → T_IsSemigroup_472 Source #

d_assoc_2336 ∷ T_IsSemigroup_472 → Bool → Bool → Bool → T__'8801'__12 Source #

d_isMagma_2340 ∷ T_IsSemigroup_472 → T_IsMagma_176 Source #

d_isSemiringWithoutAnnihilatingZero_2454 ∷ T_IsSemiring_1570 → T_IsSemiringWithoutAnnihilatingZero_1468 Source #

d_zero_2468 ∷ T_IsSemiring_1570 → T_Σ_14 Source #

d_IsBooleanAlgebra_2652 ∷ p → p → p → p → p → () Source #

d_IsDistributiveLattice_2660 ∷ p → p → () Source #

d_IsLattice_2664 ∷ p → p → () Source #

d_IsSemilattice_2668 ∷ (Bool → Bool → Bool) → () Source #

d_isDistributiveLattice_2674 ∷ T_IsBooleanAlgebra_3112 → T_IsDistributiveLattice_3036 Source #

d_'172''45'cong_2690 ∷ T_IsBooleanAlgebra_3112 → Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

d_'8743''45'complement_2698 ∷ T_IsBooleanAlgebra_3112 → T_Σ_14 Source #

d_'8744''45'complement_2722 ∷ T_IsBooleanAlgebra_3112 → T_Σ_14 Source #

d_isLattice_2884 ∷ T_IsDistributiveLattice_3036 → T_IsLattice_2962 Source #

d_'8743''45'distrib'45''8744'_2908 ∷ T_IsDistributiveLattice_3036 → T_Σ_14 Source #

d_'8744''45'distrib'45''8743'_2926 ∷ T_IsDistributiveLattice_3036 → T_Σ_14 Source #

d_absorptive_2968 ∷ T_IsLattice_2962 → T_Σ_14 Source #

d_isEquivalence_2970 ∷ T_IsLattice_2962 → T_IsEquivalence_26 Source #

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

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

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

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

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

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

d__'8799'__3082 ∷ Bool → Bool → T_Dec_20 Source #

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

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

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

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

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

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

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

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

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

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

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

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

d__'8804''63'__3108 ∷ Bool → Bool → T_Dec_20 Source #

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

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

d_'8804''45'isPartialOrder_3116 ∷ T_IsPartialOrder_174 Source #

d_'8804''45'isTotalOrder_3118 ∷ T_IsTotalOrder_404 Source #

d_'8804''45'isDecTotalOrder_3120 ∷ T_IsDecTotalOrder_460 Source #

d_'8804''45'poset_3122 ∷ T_Poset_314 Source #

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

d_'8804''45'totalOrder_3126 ∷ T_TotalOrder_764 Source #

d_'8804''45'decTotalOrder_3128 ∷ T_DecTotalOrder_866 Source #

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

d_'60''45'asym_3132 ∷ Bool → Bool → T__'60'__18 → T__'60'__18 → T_Irrelevant_20 Source #

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

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

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

d_'60''45'cmp_3140 ∷ Bool → Bool → T_Tri_158 Source #

d__'60''63'__3142 ∷ Bool → Bool → T_Dec_20 Source #

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

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

d_'60''45'wellFounded_3152 ∷ Bool → T_Acc_42 Source #

d_'60''45'acc_3162 ∷ Bool → Bool → Bool → T__'60'__18 → T_Acc_42 Source #

d_'60''45'isStrictPartialOrder_3164 ∷ T_IsStrictPartialOrder_290 Source #

d_'60''45'isStrictTotalOrder_3166 ∷ T_IsStrictTotalOrder_534 Source #

d_'60''45'strictPartialOrder_3168 ∷ T_StrictPartialOrder_556 Source #

d_'60''45'strictTotalOrder_3170 ∷ T_StrictTotalOrder_1036 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8744''45'conical'737'_3212 ∷ Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

d_'8744''45'conical'691'_3214 ∷ Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

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

d_'8744''45'isMagma_3218 ∷ T_IsMagma_176 Source #

d_'8744''45'magma_3220 ∷ T_Magma_68 Source #

d_'8744''45'isSemigroup_3222 ∷ T_IsSemigroup_472 Source #

d_'8744''45'semigroup_3224 ∷ T_Semigroup_536 Source #

d_'8744''45'isBand_3226 ∷ T_IsBand_508 Source #

d_'8744''45'band_3228 ∷ T_Band_596 Source #

d_'8744''45'isSemilattice_3230 ∷ T_IsCommutativeBand_590 Source #

d_'8744''45'semilattice_3232 ∷ T_Semilattice_10 Source #

d_'8744''45'isMonoid_3234 ∷ T_IsMonoid_686 Source #

d_'8744''45'isCommutativeMonoid_3236 ∷ T_IsCommutativeMonoid_736 Source #

d_'8744''45'commutativeMonoid_3238 ∷ T_CommutativeMonoid_962 Source #

d_'8744''45'isIdempotentCommutativeMonoid_3240 ∷ T_IsIdempotentCommutativeMonoid_852 Source #

d_'8744''45'idempotentCommutativeMonoid_3242 ∷ T_IdempotentCommutativeMonoid_1148 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

d_'8743''45'conical'737'_3284 ∷ Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

d_'8743''45'conical'691'_3286 ∷ Bool → Bool → T__'8801'__12 → T__'8801'__12 Source #

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

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

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

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

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

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

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

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

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

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

d_'8743''45'isMagma_3344 ∷ T_IsMagma_176 Source #

d_'8743''45'magma_3346 ∷ T_Magma_68 Source #

d_'8743''45'isSemigroup_3348 ∷ T_IsSemigroup_472 Source #

d_'8743''45'semigroup_3350 ∷ T_Semigroup_536 Source #

d_'8743''45'isBand_3352 ∷ T_IsBand_508 Source #

d_'8743''45'band_3354 ∷ T_Band_596 Source #

d_'8743''45'isSemilattice_3356 ∷ T_IsCommutativeBand_590 Source #

d_'8743''45'semilattice_3358 ∷ T_Semilattice_10 Source #

d_'8743''45'isMonoid_3360 ∷ T_IsMonoid_686 Source #

d_'8743''45'isCommutativeMonoid_3362 ∷ T_IsCommutativeMonoid_736 Source #

d_'8743''45'commutativeMonoid_3364 ∷ T_CommutativeMonoid_962 Source #

d_'8743''45'isIdempotentCommutativeMonoid_3366 ∷ T_IsIdempotentCommutativeMonoid_852 Source #

d_'8743''45'idempotentCommutativeMonoid_3368 ∷ T_IdempotentCommutativeMonoid_1148 Source #

d_'8744''45''8743''45'isSemiring_3370 ∷ T_IsSemiring_1570 Source #

d_'8744''45''8743''45'isCommutativeSemiring_3372 ∷ T_IsCommutativeSemiring_1678 Source #

d_'8744''45''8743''45'commutativeSemiring_3374 ∷ T_CommutativeSemiring_2446 Source #

d_'8743''45''8744''45'isSemiring_3376 ∷ T_IsSemiring_1570 Source #

d_'8743''45''8744''45'isCommutativeSemiring_3378 ∷ T_IsCommutativeSemiring_1678 Source #

d_'8743''45''8744''45'commutativeSemiring_3380 ∷ T_CommutativeSemiring_2446 Source #

d_'8744''45''8743''45'isLattice_3382 ∷ T_IsLattice_2962 Source #

d_'8744''45''8743''45'lattice_3384 ∷ T_Lattice_500 Source #

d_'8744''45''8743''45'isDistributiveLattice_3386 ∷ T_IsDistributiveLattice_3036 Source #

d_'8744''45''8743''45'distributiveLattice_3388 ∷ T_DistributiveLattice_584 Source #

d_'8744''45''8743''45'isBooleanAlgebra_3390 ∷ T_IsBooleanAlgebra_3112 Source #

d_'8744''45''8743''45'booleanAlgebra_3392 ∷ T_BooleanAlgebra_682 Source #

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

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

d_not'45''172'_3410 ∷ Bool → Bool → T__'8801'__12 → T__'8801'__12 → T_Irrelevant_20 Source #

d_'172''45'not_3416 ∷ Bool → Bool → (T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 Source #

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

d_true'45'xor_3434 ∷ Bool → T__'8801'__12 Source #

d_xor'45'same_3438 ∷ Bool → T__'8801'__12 Source #

d_not'45'distrib'737''45'xor_3444 ∷ Bool → Bool → T__'8801'__12 Source #

d_not'45'distrib'691''45'xor_3454 ∷ Bool → Bool → T__'8801'__12 Source #

d_xor'45'assoc_3460 ∷ Bool → Bool → Bool → T__'8801'__12 Source #

d_xor'45'comm_3470 ∷ Bool → Bool → T__'8801'__12 Source #

d_xor'45'identity'737'_3472 ∷ Bool → T__'8801'__12 Source #

d_xor'45'identity'691'_3474 ∷ Bool → T__'8801'__12 Source #

d_xor'45'identity_3476 ∷ T_Σ_14 Source #

d_xor'45'inverse'737'_3478 ∷ Bool → T__'8801'__12 Source #

d_xor'45'inverse'691'_3480 ∷ Bool → T__'8801'__12 Source #

d_xor'45'inverse_3484 ∷ T_Σ_14 Source #

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

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

d_'8743''45'distrib'45'xor_3506 ∷ T_Σ_14 Source #

d_xor'45'annihilates'45'not_3512 ∷ Bool → Bool → T__'8801'__12 Source #

d_xor'45''8743''45'commutativeRing_3518 ∷ T_CommutativeRing_4016 Source #

d_if'45'float_3792 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → Bool → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_T'45''8801'_3796 ∷ Bool → T_Equivalence_1714 Source #

d_T'45'not'45''8801'_3800 ∷ Bool → T_Equivalence_1714 Source #

d_T'45''8743'_3806 ∷ Bool → Bool → T_Equivalence_1714 Source #

d_T'45''8744'_3812 ∷ Bool → Bool → T_Equivalence_1714 Source #

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

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

d_'8660''8594''8801'_3828 ∷ Bool → Bool → Bool → T_Equivalence_1714 → T__'8801'__12 Source #

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