{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Data.Bool.Properties where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Bundles
import qualified MAlonzo.Code.Algebra.Lattice.Bundles
import qualified MAlonzo.Code.Algebra.Lattice.Properties.BooleanAlgebra
import qualified MAlonzo.Code.Algebra.Lattice.Structures
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Induction.WellFounded
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
d__Absorbs__8 ::
(Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d__Absorbs__8 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d__Absorbs__8 = (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d__DistributesOver__10 ::
(Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d__DistributesOver__10 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d__DistributesOver__10 = (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d__DistributesOver'691'__12 ::
(Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d__DistributesOver'691'__12 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d__DistributesOver'691'__12 = (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d__DistributesOver'737'__14 ::
(Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d__DistributesOver'737'__14 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d__DistributesOver'737'__14 = (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Absorptive_20 ::
(Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d_Absorptive_20 :: (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d_Absorptive_20 = (Bool -> Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Associative_30 :: (Bool -> Bool -> Bool) -> ()
d_Associative_30 :: (Bool -> Bool -> Bool) -> ()
d_Associative_30 = (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Commutative_34 :: (Bool -> Bool -> Bool) -> ()
d_Commutative_34 :: (Bool -> Bool -> Bool) -> ()
d_Commutative_34 = (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Conical_40 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_Conical_40 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_Conical_40 = Bool -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Idempotent_44 :: (Bool -> Bool -> Bool) -> ()
d_Idempotent_44 :: (Bool -> Bool -> Bool) -> ()
d_Idempotent_44 = (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Identity_50 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_Identity_50 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_Identity_50 = Bool -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Inverse_54 ::
Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d_Inverse_54 :: Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d_Inverse_54 = Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Involutive_58 :: (Bool -> Bool) -> ()
d_Involutive_58 :: (Bool -> Bool) -> ()
d_Involutive_58 = (Bool -> Bool) -> ()
forall a. a
erased
d_LeftConical_68 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_LeftConical_68 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_LeftConical_68 = Bool -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_LeftIdentity_76 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_LeftIdentity_76 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_LeftIdentity_76 = Bool -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_LeftInverse_78 ::
Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d_LeftInverse_78 :: Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d_LeftInverse_78 = Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_LeftZero_84 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_LeftZero_84 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_LeftZero_84 = Bool -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_RightConical_98 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_RightConical_98 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_RightConical_98 = Bool -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_RightIdentity_106 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_RightIdentity_106 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_RightIdentity_106 = Bool -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_RightInverse_108 ::
Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d_RightInverse_108 :: Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
d_RightInverse_108 = Bool -> (Bool -> Bool) -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_RightZero_114 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_RightZero_114 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_RightZero_114 = Bool -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Selective_116 :: (Bool -> Bool -> Bool) -> ()
d_Selective_116 :: (Bool -> Bool -> Bool) -> ()
d_Selective_116 = (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_Zero_134 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_Zero_134 :: Bool -> (Bool -> Bool -> Bool) -> ()
d_Zero_134 = Bool -> (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_IsBand_142 :: p -> ()
d_IsBand_142 p
a0 = ()
d_IsCommutativeMonoid_150 :: p -> p -> ()
d_IsCommutativeMonoid_150 p
a0 p
a1 = ()
d_IsCommutativeSemiring_156 :: p -> p -> p -> p -> ()
d_IsCommutativeSemiring_156 p
a0 p
a1 p
a2 p
a3 = ()
d_IsIdempotentCommutativeMonoid_164 :: p -> p -> ()
d_IsIdempotentCommutativeMonoid_164 p
a0 p
a1 = ()
d_IsMagma_182 :: p -> ()
d_IsMagma_182 p
a0 = ()
d_IsMonoid_188 :: p -> p -> ()
d_IsMonoid_188 p
a0 p
a1 = ()
d_IsSemigroup_210 :: p -> ()
d_IsSemigroup_210 p
a0 = ()
d_IsSemiring_214 :: p -> p -> p -> p -> ()
d_IsSemiring_214 p
a0 p
a1 p
a2 p
a3 = ()
d_idem_324 ::
MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_idem_324 :: T_IsBand_508 -> Bool -> T__'8801'__12
d_idem_324 = T_IsBand_508 -> Bool -> T__'8801'__12
forall a. a
erased
d_isSemigroup_332 ::
MAlonzo.Code.Algebra.Structures.T_IsBand_508 ->
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_isSemigroup_332 :: T_IsBand_508 -> T_IsSemigroup_472
d_isSemigroup_332 T_IsBand_508
v0
= (T_IsBand_508 -> T_IsSemigroup_472) -> Any -> T_IsSemigroup_472
forall a b. a -> b
coe T_IsBand_508 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.d_isSemigroup_516 (T_IsBand_508 -> Any
forall a b. a -> b
coe T_IsBand_508
v0)
d_comm_520 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736 ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_comm_520 :: T_IsCommutativeMonoid_736 -> Bool -> Bool -> T__'8801'__12
d_comm_520 = T_IsCommutativeMonoid_736 -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_isMonoid_536 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736 ->
MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_isMonoid_536 :: T_IsCommutativeMonoid_736 -> T_IsMonoid_686
d_isMonoid_536 T_IsCommutativeMonoid_736
v0
= (T_IsCommutativeMonoid_736 -> T_IsMonoid_686)
-> Any -> T_IsMonoid_686
forall a b. a -> b
coe T_IsCommutativeMonoid_736 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.d_isMonoid_746 (T_IsCommutativeMonoid_736 -> Any
forall a b. a -> b
coe T_IsCommutativeMonoid_736
v0)
d_'42''45'comm_720 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678 ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'42''45'comm_720 :: T_IsCommutativeSemiring_1678 -> Bool -> Bool -> T__'8801'__12
d_'42''45'comm_720 = T_IsCommutativeSemiring_1678 -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_isSemiring_790 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678 ->
MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570
d_isSemiring_790 :: T_IsCommutativeSemiring_1678 -> T_IsSemiring_1570
d_isSemiring_790 T_IsCommutativeSemiring_1678
v0
= (T_IsCommutativeSemiring_1678 -> T_IsSemiring_1570)
-> Any -> T_IsSemiring_1570
forall a b. a -> b
coe T_IsCommutativeSemiring_1678 -> T_IsSemiring_1570
MAlonzo.Code.Algebra.Structures.d_isSemiring_1692 (T_IsCommutativeSemiring_1678 -> Any
forall a b. a -> b
coe T_IsCommutativeSemiring_1678
v0)
d_idem_968 ::
MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_idem_968 :: T_IsIdempotentCommutativeMonoid_852 -> Bool -> T__'8801'__12
d_idem_968 = T_IsIdempotentCommutativeMonoid_852 -> Bool -> T__'8801'__12
forall a. a
erased
d_isCommutativeMonoid_982 ::
MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852 ->
MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
d_isCommutativeMonoid_982 :: T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMonoid_736
d_isCommutativeMonoid_982 T_IsIdempotentCommutativeMonoid_852
v0
= (T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMonoid_736)
-> Any -> T_IsCommutativeMonoid_736
forall a b. a -> b
coe
T_IsIdempotentCommutativeMonoid_852 -> T_IsCommutativeMonoid_736
MAlonzo.Code.Algebra.Structures.d_isCommutativeMonoid_862 (T_IsIdempotentCommutativeMonoid_852 -> Any
forall a b. a -> b
coe T_IsIdempotentCommutativeMonoid_852
v0)
d_isEquivalence_1482 ::
MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_1482 :: T_IsMagma_176 -> T_IsEquivalence_26
d_isEquivalence_1482 T_IsMagma_176
v0
= (T_IsMagma_176 -> T_IsEquivalence_26) -> Any -> T_IsEquivalence_26
forall a b. a -> b
coe T_IsMagma_176 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (T_IsMagma_176 -> Any
forall a b. a -> b
coe T_IsMagma_176
v0)
d_'8729''45'cong_1496 ::
MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
Bool ->
Bool ->
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8729''45'cong_1496 :: T_IsMagma_176
-> Bool
-> Bool
-> Bool
-> Bool
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
d_'8729''45'cong_1496 = T_IsMagma_176
-> Bool
-> Bool
-> Bool
-> Bool
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_identity_1592 ::
MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_identity_1592 :: T_IsMonoid_686 -> T_Σ_14
d_identity_1592 T_IsMonoid_686
v0
= (T_IsMonoid_686 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe T_IsMonoid_686 -> T_Σ_14
MAlonzo.Code.Algebra.Structures.d_identity_698 (T_IsMonoid_686 -> Any
forall a b. a -> b
coe T_IsMonoid_686
v0)
d_isSemigroup_1604 ::
MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_isSemigroup_1604 :: T_IsMonoid_686 -> T_IsSemigroup_472
d_isSemigroup_1604 T_IsMonoid_686
v0
= (T_IsMonoid_686 -> T_IsSemigroup_472) -> Any -> T_IsSemigroup_472
forall a b. a -> b
coe T_IsMonoid_686 -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (T_IsMonoid_686 -> Any
forall a b. a -> b
coe T_IsMonoid_686
v0)
d_assoc_2336 ::
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_assoc_2336 :: T_IsSemigroup_472 -> Bool -> Bool -> Bool -> T__'8801'__12
d_assoc_2336 = T_IsSemigroup_472 -> Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_isMagma_2340 ::
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_isMagma_2340 :: T_IsSemigroup_472 -> T_IsMagma_176
d_isMagma_2340 T_IsSemigroup_472
v0
= (T_IsSemigroup_472 -> T_IsMagma_176) -> Any -> T_IsMagma_176
forall a b. a -> b
coe T_IsSemigroup_472 -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.d_isMagma_480 (T_IsSemigroup_472 -> Any
forall a b. a -> b
coe T_IsSemigroup_472
v0)
d_isSemiringWithoutAnnihilatingZero_2454 ::
MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570 ->
MAlonzo.Code.Algebra.Structures.T_IsSemiringWithoutAnnihilatingZero_1468
d_isSemiringWithoutAnnihilatingZero_2454 :: T_IsSemiring_1570 -> T_IsSemiringWithoutAnnihilatingZero_1468
d_isSemiringWithoutAnnihilatingZero_2454 T_IsSemiring_1570
v0
= (T_IsSemiring_1570 -> T_IsSemiringWithoutAnnihilatingZero_1468)
-> Any -> T_IsSemiringWithoutAnnihilatingZero_1468
forall a b. a -> b
coe
T_IsSemiring_1570 -> T_IsSemiringWithoutAnnihilatingZero_1468
MAlonzo.Code.Algebra.Structures.d_isSemiringWithoutAnnihilatingZero_1584
(T_IsSemiring_1570 -> Any
forall a b. a -> b
coe T_IsSemiring_1570
v0)
d_zero_2468 ::
MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_zero_2468 :: T_IsSemiring_1570 -> T_Σ_14
d_zero_2468 T_IsSemiring_1570
v0
= (T_IsSemiring_1570 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe T_IsSemiring_1570 -> T_Σ_14
MAlonzo.Code.Algebra.Structures.d_zero_1586 (T_IsSemiring_1570 -> Any
forall a b. a -> b
coe T_IsSemiring_1570
v0)
d_IsBooleanAlgebra_2652 :: p -> p -> p -> p -> p -> ()
d_IsBooleanAlgebra_2652 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
d_IsDistributiveLattice_2660 :: p -> p -> ()
d_IsDistributiveLattice_2660 p
a0 p
a1 = ()
d_IsLattice_2664 :: p -> p -> ()
d_IsLattice_2664 p
a0 p
a1 = ()
d_IsSemilattice_2668 :: (Bool -> Bool -> Bool) -> ()
d_IsSemilattice_2668 :: (Bool -> Bool -> Bool) -> ()
d_IsSemilattice_2668 = (Bool -> Bool -> Bool) -> ()
forall a. a
erased
d_isDistributiveLattice_2674 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112 ->
MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
d_isDistributiveLattice_2674 :: T_IsBooleanAlgebra_3112 -> T_IsDistributiveLattice_3036
d_isDistributiveLattice_2674 T_IsBooleanAlgebra_3112
v0
= (T_IsBooleanAlgebra_3112 -> T_IsDistributiveLattice_3036)
-> Any -> T_IsDistributiveLattice_3036
forall a b. a -> b
coe
T_IsBooleanAlgebra_3112 -> T_IsDistributiveLattice_3036
MAlonzo.Code.Algebra.Lattice.Structures.d_isDistributiveLattice_3132
(T_IsBooleanAlgebra_3112 -> Any
forall a b. a -> b
coe T_IsBooleanAlgebra_3112
v0)
d_'172''45'cong_2690 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112 ->
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'172''45'cong_2690 :: T_IsBooleanAlgebra_3112
-> Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
d_'172''45'cong_2690 = T_IsBooleanAlgebra_3112
-> Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_'8743''45'complement_2698 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'complement_2698 :: T_IsBooleanAlgebra_3112 -> T_Σ_14
d_'8743''45'complement_2698 T_IsBooleanAlgebra_3112
v0
= (T_IsBooleanAlgebra_3112 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
T_IsBooleanAlgebra_3112 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'complement_3136
(T_IsBooleanAlgebra_3112 -> Any
forall a b. a -> b
coe T_IsBooleanAlgebra_3112
v0)
d_'8744''45'complement_2722 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'complement_2722 :: T_IsBooleanAlgebra_3112 -> T_Σ_14
d_'8744''45'complement_2722 T_IsBooleanAlgebra_3112
v0
= (T_IsBooleanAlgebra_3112 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
T_IsBooleanAlgebra_3112 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'complement_3134
(T_IsBooleanAlgebra_3112 -> Any
forall a b. a -> b
coe T_IsBooleanAlgebra_3112
v0)
d_isLattice_2884 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
d_isLattice_2884 :: T_IsDistributiveLattice_3036 -> T_IsLattice_2962
d_isLattice_2884 T_IsDistributiveLattice_3036
v0
= (T_IsDistributiveLattice_3036 -> T_IsLattice_2962)
-> Any -> T_IsLattice_2962
forall a b. a -> b
coe
T_IsDistributiveLattice_3036 -> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Structures.d_isLattice_3048 (T_IsDistributiveLattice_3036 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3036
v0)
d_'8743''45'distrib'45''8744'_2908 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'distrib'45''8744'_2908 :: T_IsDistributiveLattice_3036 -> T_Σ_14
d_'8743''45'distrib'45''8744'_2908 T_IsDistributiveLattice_3036
v0
= (T_IsDistributiveLattice_3036 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
T_IsDistributiveLattice_3036 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8743''45'distrib'45''8744'_3052
(T_IsDistributiveLattice_3036 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3036
v0)
d_'8744''45'distrib'45''8743'_2926 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'distrib'45''8743'_2926 :: T_IsDistributiveLattice_3036 -> T_Σ_14
d_'8744''45'distrib'45''8743'_2926 T_IsDistributiveLattice_3036
v0
= (T_IsDistributiveLattice_3036 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
T_IsDistributiveLattice_3036 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_'8744''45'distrib'45''8743'_3050
(T_IsDistributiveLattice_3036 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3036
v0)
d_absorptive_2968 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_absorptive_2968 :: T_IsLattice_2962 -> T_Σ_14
d_absorptive_2968 T_IsLattice_2962
v0
= (T_IsLattice_2962 -> T_Σ_14) -> Any -> T_Σ_14
forall a b. a -> b
coe
T_IsLattice_2962 -> T_Σ_14
MAlonzo.Code.Algebra.Lattice.Structures.d_absorptive_2998 (T_IsLattice_2962 -> Any
forall a b. a -> b
coe T_IsLattice_2962
v0)
d_isEquivalence_2970 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
d_isEquivalence_2970 :: T_IsLattice_2962 -> T_IsEquivalence_26
d_isEquivalence_2970 T_IsLattice_2962
v0
= (T_IsLattice_2962 -> T_IsEquivalence_26)
-> Any -> T_IsEquivalence_26
forall a b. a -> b
coe
T_IsLattice_2962 -> T_IsEquivalence_26
MAlonzo.Code.Algebra.Lattice.Structures.d_isEquivalence_2984
(T_IsLattice_2962 -> Any
forall a b. a -> b
coe T_IsLattice_2962
v0)
d_'8743''45'assoc_2984 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'assoc_2984 :: T_IsLattice_2962 -> Bool -> Bool -> Bool -> T__'8801'__12
d_'8743''45'assoc_2984 = T_IsLattice_2962 -> Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'comm_2986 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'comm_2986 :: T_IsLattice_2962 -> Bool -> Bool -> T__'8801'__12
d_'8743''45'comm_2986 = T_IsLattice_2962 -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'cong_2988 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
Bool ->
Bool ->
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.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_'8743''45'cong_2988 = T_IsLattice_2962
-> Bool
-> Bool
-> Bool
-> Bool
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_'8744''45'assoc_2996 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'assoc_2996 :: T_IsLattice_2962 -> Bool -> Bool -> Bool -> T__'8801'__12
d_'8744''45'assoc_2996 = T_IsLattice_2962 -> Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'comm_2998 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'comm_2998 :: T_IsLattice_2962 -> Bool -> Bool -> T__'8801'__12
d_'8744''45'comm_2998 = T_IsLattice_2962 -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'cong_3000 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962 ->
Bool ->
Bool ->
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.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_'8744''45'cong_3000 = T_IsLattice_2962
-> Bool
-> Bool
-> Bool
-> Bool
-> T__'8801'__12
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d__'8799'__3082 ::
Bool ->
Bool -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__3082 :: Bool -> Bool -> T_Dec_20
d__'8799'__3082 Bool
v0 Bool
v1
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v1)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
forall a. a
erased)
else (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v1) (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
else (if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v0) (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
else (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
forall a. a
erased))
d_'8801''45'setoid_3084 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
d_'8801''45'setoid_3084 :: T_Setoid_44
d_'8801''45'setoid_3084
= T_Setoid_44 -> T_Setoid_44
forall a b. a -> b
coe
T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402
d_'8801''45'decSetoid_3086 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
d_'8801''45'decSetoid_3086 :: T_DecSetoid_84
d_'8801''45'decSetoid_3086
= ((Any -> Any -> T_Dec_20) -> T_DecSetoid_84)
-> Any -> T_DecSetoid_84
forall a b. a -> b
coe
(Any -> Any -> T_Dec_20) -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
((Bool -> Bool -> T_Dec_20) -> Any
forall a b. a -> b
coe Bool -> Bool -> T_Dec_20
d__'8799'__3082)
d_'8804''45'reflexive_3088 ::
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10
d_'8804''45'reflexive_3088 :: Bool -> Bool -> T__'8801'__12 -> T__'8804'__10
d_'8804''45'reflexive_3088 ~Bool
v0 ~Bool
v1 ~T__'8801'__12
v2
= T__'8804'__10
du_'8804''45'reflexive_3088
du_'8804''45'reflexive_3088 ::
MAlonzo.Code.Data.Bool.Base.T__'8804'__10
du_'8804''45'reflexive_3088 :: T__'8804'__10
du_'8804''45'reflexive_3088
= T__'8804'__10 -> T__'8804'__10
forall a b. a -> b
coe T__'8804'__10
MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16
d_'8804''45'refl_3090 ::
Bool -> MAlonzo.Code.Data.Bool.Base.T__'8804'__10
d_'8804''45'refl_3090 :: Bool -> T__'8804'__10
d_'8804''45'refl_3090 ~Bool
v0 = T__'8804'__10
du_'8804''45'refl_3090
du_'8804''45'refl_3090 :: MAlonzo.Code.Data.Bool.Base.T__'8804'__10
du_'8804''45'refl_3090 :: T__'8804'__10
du_'8804''45'refl_3090 = T__'8804'__10 -> T__'8804'__10
forall a b. a -> b
coe T__'8804'__10
du_'8804''45'reflexive_3088
d_'8804''45'trans_3092 ::
Bool ->
Bool ->
Bool ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10
d_'8804''45'trans_3092 :: Bool
-> Bool -> Bool -> T__'8804'__10 -> T__'8804'__10 -> T__'8804'__10
d_'8804''45'trans_3092 ~Bool
v0 ~Bool
v1 ~Bool
v2 T__'8804'__10
v3 T__'8804'__10
v4
= T__'8804'__10 -> T__'8804'__10 -> T__'8804'__10
du_'8804''45'trans_3092 T__'8804'__10
v3 T__'8804'__10
v4
du_'8804''45'trans_3092 ::
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10
du_'8804''45'trans_3092 :: T__'8804'__10 -> T__'8804'__10 -> T__'8804'__10
du_'8804''45'trans_3092 T__'8804'__10
v0 T__'8804'__10
v1
= case T__'8804'__10 -> T__'8804'__10
forall a b. a -> b
coe T__'8804'__10
v0 of
T__'8804'__10
MAlonzo.Code.Data.Bool.Base.C_f'8804't_12
-> (Any -> Any -> Any) -> Any -> Any -> T__'8804'__10
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T__'8804'__10 -> Any
forall a b. a -> b
coe T__'8804'__10
v1) (T__'8804'__10 -> Any
forall a b. a -> b
coe T__'8804'__10
v0)
T__'8804'__10
MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16 -> T__'8804'__10 -> T__'8804'__10
forall a b. a -> b
coe T__'8804'__10
v1
T__'8804'__10
_ -> T__'8804'__10
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'8804''45'antisym_3096 ::
Bool ->
Bool ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8804''45'antisym_3096 :: Bool -> Bool -> T__'8804'__10 -> T__'8804'__10 -> T__'8801'__12
d_'8804''45'antisym_3096 = Bool -> Bool -> T__'8804'__10 -> T__'8804'__10 -> T__'8801'__12
forall a. a
erased
d_'8804''45'minimum_3098 ::
Bool -> MAlonzo.Code.Data.Bool.Base.T__'8804'__10
d_'8804''45'minimum_3098 :: Bool -> T__'8804'__10
d_'8804''45'minimum_3098 Bool
v0
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then T__'8804'__10 -> T__'8804'__10
forall a b. a -> b
coe T__'8804'__10
MAlonzo.Code.Data.Bool.Base.C_f'8804't_12
else T__'8804'__10 -> T__'8804'__10
forall a b. a -> b
coe T__'8804'__10
MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16
d_'8804''45'maximum_3100 ::
Bool -> MAlonzo.Code.Data.Bool.Base.T__'8804'__10
d_'8804''45'maximum_3100 :: Bool -> T__'8804'__10
d_'8804''45'maximum_3100 Bool
v0
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then T__'8804'__10 -> T__'8804'__10
forall a b. a -> b
coe T__'8804'__10
MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16
else T__'8804'__10 -> T__'8804'__10
forall a b. a -> b
coe T__'8804'__10
MAlonzo.Code.Data.Bool.Base.C_f'8804't_12
d_'8804''45'total_3102 ::
Bool -> Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8804''45'total_3102 :: Bool -> Bool -> T__'8846'__30
d_'8804''45'total_3102 Bool
v0 Bool
v1
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe
Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
((Bool -> T__'8804'__10) -> Any -> Any
forall a b. a -> b
coe Bool -> T__'8804'__10
d_'8804''45'maximum_3100 (Bool -> Any
forall a b. a -> b
coe Bool
v1))
else (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe
Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
((Bool -> T__'8804'__10) -> Any -> Any
forall a b. a -> b
coe Bool -> T__'8804'__10
d_'8804''45'minimum_3098 (Bool -> Any
forall a b. a -> b
coe Bool
v1))
d__'8804''63'__3108 ::
Bool ->
Bool -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8804''63'__3108 :: Bool -> Bool -> T_Dec_20
d__'8804''63'__3108 Bool
v0 Bool
v1
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v1)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T__'8804'__10 -> Any
forall a b. a -> b
coe T__'8804'__10
MAlonzo.Code.Data.Bool.Base.C_b'8804'b_16))
else (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v1) (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
else (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((Bool -> T__'8804'__10) -> Any -> Any
forall a b. a -> b
coe Bool -> T__'8804'__10
d_'8804''45'minimum_3098 (Bool -> Any
forall a b. a -> b
coe Bool
v1)))
d_'8804''45'irrelevant_3112 ::
Bool ->
Bool ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8804''45'irrelevant_3112 :: Bool -> Bool -> T__'8804'__10 -> T__'8804'__10 -> T__'8801'__12
d_'8804''45'irrelevant_3112 = Bool -> Bool -> T__'8804'__10 -> T__'8804'__10 -> T__'8801'__12
forall a. a
erased
d_'8804''45'isPreorder_3114 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8804''45'isPreorder_3114 :: T_IsPreorder_70
d_'8804''45'isPreorder_3114
= (T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70)
-> Any
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70
forall a b. a -> b
coe
T_IsEquivalence_26
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
(\ Any
v0 Any
v1 Any
v2 -> T__'8804'__10 -> Any
forall a b. a -> b
coe T__'8804'__10
du_'8804''45'reflexive_3088)
(\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T__'8804'__10 -> T__'8804'__10 -> T__'8804'__10)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8804'__10 -> T__'8804'__10 -> T__'8804'__10
du_'8804''45'trans_3092 Any
v3 Any
v4)
d_'8804''45'isPartialOrder_3116 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_'8804''45'isPartialOrder_3116 :: T_IsPartialOrder_174
d_'8804''45'isPartialOrder_3116
= (T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_174)
-> Any -> Any -> T_IsPartialOrder_174
forall a b. a -> b
coe
T_IsPreorder_70
-> (Any -> Any -> Any -> Any -> Any) -> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
(T_IsPreorder_70 -> Any
forall a b. a -> b
coe T_IsPreorder_70
d_'8804''45'isPreorder_3114) Any
forall a. a
erased
d_'8804''45'isTotalOrder_3118 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_404
d_'8804''45'isTotalOrder_3118 :: T_IsTotalOrder_404
d_'8804''45'isTotalOrder_3118
= (T_IsPartialOrder_174
-> (Any -> Any -> T__'8846'__30) -> T_IsTotalOrder_404)
-> Any -> Any -> T_IsTotalOrder_404
forall a b. a -> b
coe
T_IsPartialOrder_174
-> (Any -> Any -> T__'8846'__30) -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_20555
(T_IsPartialOrder_174 -> Any
forall a b. a -> b
coe T_IsPartialOrder_174
d_'8804''45'isPartialOrder_3116) ((Bool -> Bool -> T__'8846'__30) -> Any
forall a b. a -> b
coe Bool -> Bool -> T__'8846'__30
d_'8804''45'total_3102)
d_'8804''45'isDecTotalOrder_3120 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460
d_'8804''45'isDecTotalOrder_3120 :: T_IsDecTotalOrder_460
d_'8804''45'isDecTotalOrder_3120
= (T_IsTotalOrder_404
-> (Any -> Any -> T_Dec_20)
-> (Any -> Any -> T_Dec_20)
-> T_IsDecTotalOrder_460)
-> Any -> Any -> Any -> T_IsDecTotalOrder_460
forall a b. a -> b
coe
T_IsTotalOrder_404
-> (Any -> Any -> T_Dec_20)
-> (Any -> Any -> T_Dec_20)
-> T_IsDecTotalOrder_460
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_22695
(T_IsTotalOrder_404 -> Any
forall a b. a -> b
coe T_IsTotalOrder_404
d_'8804''45'isTotalOrder_3118) ((Bool -> Bool -> T_Dec_20) -> Any
forall a b. a -> b
coe Bool -> Bool -> T_Dec_20
d__'8799'__3082)
((Bool -> Bool -> T_Dec_20) -> Any
forall a b. a -> b
coe Bool -> Bool -> T_Dec_20
d__'8804''63'__3108)
d_'8804''45'poset_3122 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_'8804''45'poset_3122 :: T_Poset_314
d_'8804''45'poset_3122
= (T_IsPartialOrder_174 -> T_Poset_314)
-> T_IsPartialOrder_174 -> T_Poset_314
forall a b. a -> b
coe
T_IsPartialOrder_174 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
T_IsPartialOrder_174
d_'8804''45'isPartialOrder_3116
d_'8804''45'preorder_3124 ::
MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_'8804''45'preorder_3124 :: T_Preorder_132
d_'8804''45'preorder_3124
= (T_IsPreorder_70 -> T_Preorder_132)
-> T_IsPreorder_70 -> T_Preorder_132
forall a b. a -> b
coe
T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
T_IsPreorder_70
d_'8804''45'isPreorder_3114
d_'8804''45'totalOrder_3126 ::
MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_764
d_'8804''45'totalOrder_3126 :: T_TotalOrder_764
d_'8804''45'totalOrder_3126
= (T_IsTotalOrder_404 -> T_TotalOrder_764)
-> T_IsTotalOrder_404 -> T_TotalOrder_764
forall a b. a -> b
coe
T_IsTotalOrder_404 -> T_TotalOrder_764
MAlonzo.Code.Relation.Binary.Bundles.C_TotalOrder'46'constructor_15747
T_IsTotalOrder_404
d_'8804''45'isTotalOrder_3118
d_'8804''45'decTotalOrder_3128 ::
MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_866
d_'8804''45'decTotalOrder_3128 :: T_DecTotalOrder_866
d_'8804''45'decTotalOrder_3128
= (T_IsDecTotalOrder_460 -> T_DecTotalOrder_866)
-> T_IsDecTotalOrder_460 -> T_DecTotalOrder_866
forall a b. a -> b
coe
T_IsDecTotalOrder_460 -> T_DecTotalOrder_866
MAlonzo.Code.Relation.Binary.Bundles.C_DecTotalOrder'46'constructor_17849
T_IsDecTotalOrder_460
d_'8804''45'isDecTotalOrder_3120
d_'60''45'irrefl_3130 ::
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''45'irrefl_3130 :: Bool -> Bool -> T__'8801'__12 -> T__'60'__18 -> T_Irrelevant_20
d_'60''45'irrefl_3130 = Bool -> Bool -> T__'8801'__12 -> T__'60'__18 -> T_Irrelevant_20
forall a. a
erased
d_'60''45'asym_3132 ::
Bool ->
Bool ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'60''45'asym_3132 :: Bool -> Bool -> T__'60'__18 -> T__'60'__18 -> T_Irrelevant_20
d_'60''45'asym_3132 = Bool -> Bool -> T__'60'__18 -> T__'60'__18 -> T_Irrelevant_20
forall a. a
erased
d_'60''45'trans_3134 ::
Bool ->
Bool ->
Bool ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18
d_'60''45'trans_3134 :: Bool -> Bool -> Bool -> T__'60'__18 -> T__'60'__18 -> T__'60'__18
d_'60''45'trans_3134 = Bool -> Bool -> Bool -> T__'60'__18 -> T__'60'__18 -> T__'60'__18
forall a. a
erased
d_'60''45'trans'691'_3136 ::
Bool ->
Bool ->
Bool ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Data.Bool.Base.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'691'_3136 = Bool -> Bool -> Bool -> T__'8804'__10 -> T__'60'__18 -> T__'60'__18
forall a. a
erased
d_'60''45'trans'737'_3138 ::
Bool ->
Bool ->
Bool ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Data.Bool.Base.T__'8804'__10 ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18
d_'60''45'trans'737'_3138 :: Bool -> Bool -> Bool -> T__'60'__18 -> T__'8804'__10 -> T__'60'__18
d_'60''45'trans'737'_3138 = Bool -> Bool -> Bool -> T__'60'__18 -> T__'8804'__10 -> T__'60'__18
forall a. a
erased
d_'60''45'cmp_3140 ::
Bool -> Bool -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
d_'60''45'cmp_3140 :: Bool -> Bool -> T_Tri_158
d_'60''45'cmp_3140 Bool
v0 Bool
v1
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (Any -> T_Tri_158) -> Any -> T_Tri_158
forall a b. a -> b
coe
Any -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 Any
forall a. a
erased
else (Any -> T_Tri_158) -> Any -> T_Tri_158
forall a b. a -> b
coe
Any -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 Any
forall a. a
erased
else (if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (Any -> T_Tri_158) -> Any -> T_Tri_158
forall a b. a -> b
coe
Any -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 Any
forall a. a
erased
else (Any -> T_Tri_158) -> Any -> T_Tri_158
forall a b. a -> b
coe
Any -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 Any
forall a. a
erased)
d__'60''63'__3142 ::
Bool ->
Bool -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'60''63'__3142 :: Bool -> Bool -> T_Dec_20
d__'60''63'__3142 Bool
v0 Bool
v1
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
else (if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v1)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
forall a. a
erased)
else (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v1)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
d_'60''45'resp'8322''45''8801'_3144 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'resp'8322''45''8801'_3144 :: T_Σ_14
d_'60''45'resp'8322''45''8801'_3144
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> Any
v4)) ((Any -> Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> Any
v4))
d_'60''45'irrelevant_3150 ::
Bool ->
Bool ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'60''45'irrelevant_3150 :: Bool -> Bool -> T__'60'__18 -> T__'60'__18 -> T__'8801'__12
d_'60''45'irrelevant_3150 = Bool -> Bool -> T__'60'__18 -> T__'60'__18 -> T__'8801'__12
forall a. a
erased
d_'60''45'wellFounded_3152 ::
Bool -> MAlonzo.Code.Induction.WellFounded.T_Acc_42
d_'60''45'wellFounded_3152 :: Bool -> T_Acc_42
d_'60''45'wellFounded_3152 = Bool -> T_Acc_42
forall a. a
erased
d_'60''45'acc_3162 ::
Bool ->
Bool ->
Bool ->
MAlonzo.Code.Data.Bool.Base.T__'60'__18 ->
MAlonzo.Code.Induction.WellFounded.T_Acc_42
d_'60''45'acc_3162 :: Bool -> Bool -> Bool -> T__'60'__18 -> T_Acc_42
d_'60''45'acc_3162 = Bool -> Bool -> Bool -> T__'60'__18 -> T_Acc_42
forall a. a
erased
d_'60''45'isStrictPartialOrder_3164 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_3164 :: T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_3164
= (T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_IsStrictPartialOrder_290)
-> Any -> Any -> T_Σ_14 -> T_IsStrictPartialOrder_290
forall a b. a -> b
coe
T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_14045
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
Any
forall a. a
erased T_Σ_14
d_'60''45'resp'8322''45''8801'_3144
d_'60''45'isStrictTotalOrder_3166 ::
MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder_3166 :: T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder_3166
= (T_IsStrictPartialOrder_290
-> (Any -> Any -> T_Tri_158) -> T_IsStrictTotalOrder_534)
-> Any -> Any -> T_IsStrictTotalOrder_534
forall a b. a -> b
coe
T_IsStrictPartialOrder_290
-> (Any -> Any -> T_Tri_158) -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_24953
(T_IsStrictPartialOrder_290 -> Any
forall a b. a -> b
coe T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_3164) ((Bool -> Bool -> T_Tri_158) -> Any
forall a b. a -> b
coe Bool -> Bool -> T_Tri_158
d_'60''45'cmp_3140)
d_'60''45'strictPartialOrder_3168 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
d_'60''45'strictPartialOrder_3168 :: T_StrictPartialOrder_556
d_'60''45'strictPartialOrder_3168
= (T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556)
-> T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556
forall a b. a -> b
coe
T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_11097
T_IsStrictPartialOrder_290
d_'60''45'isStrictPartialOrder_3164
d_'60''45'strictTotalOrder_3170 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder_3170 :: T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder_3170
= (T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036)
-> T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036
forall a b. a -> b
coe
T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036
MAlonzo.Code.Relation.Binary.Bundles.C_StrictTotalOrder'46'constructor_21059
T_IsStrictTotalOrder_534
d_'60''45'isStrictTotalOrder_3166
d_'8744''45'assoc_3172 ::
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'assoc_3172 :: Bool -> Bool -> Bool -> T__'8801'__12
d_'8744''45'assoc_3172 = Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'comm_3182 ::
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'comm_3182 :: Bool -> Bool -> T__'8801'__12
d_'8744''45'comm_3182 = Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'identity'737'_3184 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'identity'737'_3184 :: Bool -> T__'8801'__12
d_'8744''45'identity'737'_3184 = Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'identity'691'_3186 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'identity'691'_3186 :: Bool -> T__'8801'__12
d_'8744''45'identity'691'_3186 = Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'identity_3188 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'identity_3188 :: T_Σ_14
d_'8744''45'identity_3188
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8744''45'zero'737'_3190 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'zero'737'_3190 :: Bool -> T__'8801'__12
d_'8744''45'zero'737'_3190 = Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'zero'691'_3192 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'zero'691'_3192 :: Bool -> T__'8801'__12
d_'8744''45'zero'691'_3192 = Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'zero_3194 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'zero_3194 :: T_Σ_14
d_'8744''45'zero_3194
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8744''45'inverse'737'_3196 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'inverse'737'_3196 :: Bool -> T__'8801'__12
d_'8744''45'inverse'737'_3196 = Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'inverse'691'_3198 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'inverse'691'_3198 :: Bool -> T__'8801'__12
d_'8744''45'inverse'691'_3198 = Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'inverse_3202 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'inverse_3202 :: T_Σ_14
d_'8744''45'inverse_3202
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8744''45'idem_3204 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'idem_3204 :: Bool -> T__'8801'__12
d_'8744''45'idem_3204 = Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'sel_3206 ::
Bool -> Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8744''45'sel_3206 :: Bool -> Bool -> T__'8846'__30
d_'8744''45'sel_3206 Bool
v0 ~Bool
v1 = Bool -> T__'8846'__30
du_'8744''45'sel_3206 Bool
v0
du_'8744''45'sel_3206 ::
Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8744''45'sel_3206 :: Bool -> T__'8846'__30
du_'8744''45'sel_3206 Bool
v0
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
forall a. a
erased
else (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
forall a. a
erased
d_'8744''45'conical'737'_3212 ::
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'conical'737'_3212 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
d_'8744''45'conical'737'_3212 = Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_'8744''45'conical'691'_3214 ::
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'conical'691'_3214 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
d_'8744''45'conical'691'_3214 = Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_'8744''45'conical_3216 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'conical_3216 :: T_Σ_14
d_'8744''45'conical_3216
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8744''45'isMagma_3218 ::
MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8744''45'isMagma_3218 :: T_IsMagma_176
d_'8744''45'isMagma_3218
= (T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsMagma_176)
-> Any -> Any -> T_IsMagma_176
forall a b. a -> b
coe
T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any) -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
Any
forall a. a
erased
d_'8744''45'magma_3220 :: MAlonzo.Code.Algebra.Bundles.T_Magma_68
d_'8744''45'magma_3220 :: T_Magma_68
d_'8744''45'magma_3220
= ((Any -> Any -> Any) -> T_IsMagma_176 -> T_Magma_68)
-> (Bool -> Bool -> Bool) -> T_IsMagma_176 -> T_Magma_68
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_IsMagma_176 -> T_Magma_68
MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_1279
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30 T_IsMagma_176
d_'8744''45'isMagma_3218
d_'8744''45'isSemigroup_3222 ::
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8744''45'isSemigroup_3222 :: T_IsSemigroup_472
d_'8744''45'isSemigroup_3222
= (T_IsMagma_176 -> (Any -> Any -> Any -> Any) -> T_IsSemigroup_472)
-> Any -> Any -> T_IsSemigroup_472
forall a b. a -> b
coe
T_IsMagma_176 -> (Any -> Any -> Any -> Any) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
(T_IsMagma_176 -> Any
forall a b. a -> b
coe T_IsMagma_176
d_'8744''45'isMagma_3218) Any
forall a. a
erased
d_'8744''45'semigroup_3224 ::
MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_'8744''45'semigroup_3224 :: T_Semigroup_536
d_'8744''45'semigroup_3224
= ((Any -> Any -> Any) -> T_IsSemigroup_472 -> T_Semigroup_536)
-> (Bool -> Bool -> Bool) -> T_IsSemigroup_472 -> T_Semigroup_536
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_IsSemigroup_472 -> T_Semigroup_536
MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_9793
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
T_IsSemigroup_472
d_'8744''45'isSemigroup_3222
d_'8744''45'isBand_3226 ::
MAlonzo.Code.Algebra.Structures.T_IsBand_508
d_'8744''45'isBand_3226 :: T_IsBand_508
d_'8744''45'isBand_3226
= (T_IsSemigroup_472 -> (Any -> Any) -> T_IsBand_508)
-> Any -> Any -> T_IsBand_508
forall a b. a -> b
coe
T_IsSemigroup_472 -> (Any -> Any) -> T_IsBand_508
MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_11205
(T_IsSemigroup_472 -> Any
forall a b. a -> b
coe T_IsSemigroup_472
d_'8744''45'isSemigroup_3222) Any
forall a. a
erased
d_'8744''45'band_3228 :: MAlonzo.Code.Algebra.Bundles.T_Band_596
d_'8744''45'band_3228 :: T_Band_596
d_'8744''45'band_3228
= ((Any -> Any -> Any) -> T_IsBand_508 -> T_Band_596)
-> (Bool -> Bool -> Bool) -> T_IsBand_508 -> T_Band_596
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_IsBand_508 -> T_Band_596
MAlonzo.Code.Algebra.Bundles.C_Band'46'constructor_10881
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30 T_IsBand_508
d_'8744''45'isBand_3226
d_'8744''45'isSemilattice_3230 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
d_'8744''45'isSemilattice_3230 :: T_IsCommutativeBand_590
d_'8744''45'isSemilattice_3230
= (T_IsBand_508 -> (Any -> Any -> Any) -> T_IsCommutativeBand_590)
-> Any -> Any -> T_IsCommutativeBand_590
forall a b. a -> b
coe
T_IsBand_508 -> (Any -> Any -> Any) -> T_IsCommutativeBand_590
MAlonzo.Code.Algebra.Structures.C_IsCommutativeBand'46'constructor_13109
(T_IsBand_508 -> Any
forall a b. a -> b
coe T_IsBand_508
d_'8744''45'isBand_3226) Any
forall a. a
erased
d_'8744''45'semilattice_3232 ::
MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8744''45'semilattice_3232 :: T_Semilattice_10
d_'8744''45'semilattice_3232
= ((Any -> Any -> Any)
-> T_IsCommutativeBand_590 -> T_Semilattice_10)
-> (Bool -> Bool -> Bool)
-> T_IsCommutativeBand_590
-> T_Semilattice_10
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_IsCommutativeBand_590 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Bundles.C_Semilattice'46'constructor_193
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
T_IsCommutativeBand_590
d_'8744''45'isSemilattice_3230
d_'8744''45'isMonoid_3234 ::
MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_'8744''45'isMonoid_3234 :: T_IsMonoid_686
d_'8744''45'isMonoid_3234
= (T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686)
-> Any -> Any -> T_IsMonoid_686
forall a b. a -> b
coe
T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
(T_IsSemigroup_472 -> Any
forall a b. a -> b
coe T_IsSemigroup_472
d_'8744''45'isSemigroup_3222) (T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8744''45'identity_3188)
d_'8744''45'isCommutativeMonoid_3236 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
d_'8744''45'isCommutativeMonoid_3236 :: T_IsCommutativeMonoid_736
d_'8744''45'isCommutativeMonoid_3236
= (T_IsMonoid_686
-> (Any -> Any -> Any) -> T_IsCommutativeMonoid_736)
-> Any -> Any -> T_IsCommutativeMonoid_736
forall a b. a -> b
coe
T_IsMonoid_686 -> (Any -> Any -> Any) -> T_IsCommutativeMonoid_736
MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_17695
(T_IsMonoid_686 -> Any
forall a b. a -> b
coe T_IsMonoid_686
d_'8744''45'isMonoid_3234) Any
forall a. a
erased
d_'8744''45'commutativeMonoid_3238 ::
MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
d_'8744''45'commutativeMonoid_3238 :: T_CommutativeMonoid_962
d_'8744''45'commutativeMonoid_3238
= ((Any -> Any -> Any)
-> Any -> T_IsCommutativeMonoid_736 -> T_CommutativeMonoid_962)
-> (Bool -> Bool -> Bool)
-> Any
-> T_IsCommutativeMonoid_736
-> T_CommutativeMonoid_962
forall a b. a -> b
coe
(Any -> Any -> Any)
-> Any -> T_IsCommutativeMonoid_736 -> T_CommutativeMonoid_962
MAlonzo.Code.Algebra.Bundles.C_CommutativeMonoid'46'constructor_17931
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
T_IsCommutativeMonoid_736
d_'8744''45'isCommutativeMonoid_3236
d_'8744''45'isIdempotentCommutativeMonoid_3240 ::
MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852
d_'8744''45'isIdempotentCommutativeMonoid_3240 :: T_IsIdempotentCommutativeMonoid_852
d_'8744''45'isIdempotentCommutativeMonoid_3240
= (T_IsCommutativeMonoid_736
-> (Any -> Any) -> T_IsIdempotentCommutativeMonoid_852)
-> Any -> Any -> T_IsIdempotentCommutativeMonoid_852
forall a b. a -> b
coe
T_IsCommutativeMonoid_736
-> (Any -> Any) -> T_IsIdempotentCommutativeMonoid_852
MAlonzo.Code.Algebra.Structures.C_IsIdempotentCommutativeMonoid'46'constructor_20685
(T_IsCommutativeMonoid_736 -> Any
forall a b. a -> b
coe T_IsCommutativeMonoid_736
d_'8744''45'isCommutativeMonoid_3236) Any
forall a. a
erased
d_'8744''45'idempotentCommutativeMonoid_3242 ::
MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148
d_'8744''45'idempotentCommutativeMonoid_3242 :: T_IdempotentCommutativeMonoid_1148
d_'8744''45'idempotentCommutativeMonoid_3242
= ((Any -> Any -> Any)
-> Any
-> T_IsIdempotentCommutativeMonoid_852
-> T_IdempotentCommutativeMonoid_1148)
-> (Bool -> Bool -> Bool)
-> Any
-> T_IsIdempotentCommutativeMonoid_852
-> T_IdempotentCommutativeMonoid_1148
forall a b. a -> b
coe
(Any -> Any -> Any)
-> Any
-> T_IsIdempotentCommutativeMonoid_852
-> T_IdempotentCommutativeMonoid_1148
MAlonzo.Code.Algebra.Bundles.C_IdempotentCommutativeMonoid'46'constructor_21499
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
T_IsIdempotentCommutativeMonoid_852
d_'8744''45'isIdempotentCommutativeMonoid_3240
d_'8743''45'assoc_3244 ::
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'assoc_3244 :: Bool -> Bool -> Bool -> T__'8801'__12
d_'8743''45'assoc_3244 = Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'comm_3254 ::
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'comm_3254 :: Bool -> Bool -> T__'8801'__12
d_'8743''45'comm_3254 = Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'identity'737'_3256 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'identity'737'_3256 :: Bool -> T__'8801'__12
d_'8743''45'identity'737'_3256 = Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'identity'691'_3258 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'identity'691'_3258 :: Bool -> T__'8801'__12
d_'8743''45'identity'691'_3258 = Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'identity_3260 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'identity_3260 :: T_Σ_14
d_'8743''45'identity_3260
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8743''45'zero'737'_3262 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'zero'737'_3262 :: Bool -> T__'8801'__12
d_'8743''45'zero'737'_3262 = Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'zero'691'_3264 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'zero'691'_3264 :: Bool -> T__'8801'__12
d_'8743''45'zero'691'_3264 = Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'zero_3266 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'zero_3266 :: T_Σ_14
d_'8743''45'zero_3266
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8743''45'inverse'737'_3268 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'inverse'737'_3268 :: Bool -> T__'8801'__12
d_'8743''45'inverse'737'_3268 = Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'inverse'691'_3270 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'inverse'691'_3270 :: Bool -> T__'8801'__12
d_'8743''45'inverse'691'_3270 = Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'inverse_3274 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'inverse_3274 :: T_Σ_14
d_'8743''45'inverse_3274
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8743''45'idem_3276 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'idem_3276 :: Bool -> T__'8801'__12
d_'8743''45'idem_3276 = Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'sel_3278 ::
Bool -> Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8743''45'sel_3278 :: Bool -> Bool -> T__'8846'__30
d_'8743''45'sel_3278 Bool
v0 ~Bool
v1 = Bool -> T__'8846'__30
du_'8743''45'sel_3278 Bool
v0
du_'8743''45'sel_3278 ::
Bool -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8743''45'sel_3278 :: Bool -> T__'8846'__30
du_'8743''45'sel_3278 Bool
v0
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 Any
forall a. a
erased
else (Any -> T__'8846'__30) -> Any -> T__'8846'__30
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 Any
forall a. a
erased
d_'8743''45'conical'737'_3284 ::
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'conical'737'_3284 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
d_'8743''45'conical'737'_3284 = Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_'8743''45'conical'691'_3286 ::
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'conical'691'_3286 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
d_'8743''45'conical'691'_3286 = Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_'8743''45'conical_3288 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'conical_3288 :: T_Σ_14
d_'8743''45'conical_3288
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8743''45'distrib'737''45''8744'_3290 ::
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'distrib'737''45''8744'_3290 :: Bool -> Bool -> Bool -> T__'8801'__12
d_'8743''45'distrib'737''45''8744'_3290 = Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'distrib'691''45''8744'_3300 ::
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'distrib'691''45''8744'_3300 :: Bool -> Bool -> Bool -> T__'8801'__12
d_'8743''45'distrib'691''45''8744'_3300 = Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'distrib'45''8744'_3308 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'distrib'45''8744'_3308 :: T_Σ_14
d_'8743''45'distrib'45''8744'_3308
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8744''45'distrib'737''45''8743'_3310 ::
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'distrib'737''45''8743'_3310 :: Bool -> Bool -> Bool -> T__'8801'__12
d_'8744''45'distrib'737''45''8743'_3310 = Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'distrib'691''45''8743'_3320 ::
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'distrib'691''45''8743'_3320 :: Bool -> Bool -> Bool -> T__'8801'__12
d_'8744''45'distrib'691''45''8743'_3320 = Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'distrib'45''8743'_3328 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45'distrib'45''8743'_3328 :: T_Σ_14
d_'8744''45'distrib'45''8743'_3328
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8743''45'abs'45''8744'_3330 ::
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'abs'45''8744'_3330 :: Bool -> Bool -> T__'8801'__12
d_'8743''45'abs'45''8744'_3330 = Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45'abs'45''8743'_3336 ::
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8744''45'abs'45''8743'_3336 :: Bool -> Bool -> T__'8801'__12
d_'8744''45'abs'45''8743'_3336 = Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8744''45''8743''45'absorptive_3342 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8744''45''8743''45'absorptive_3342 :: T_Σ_14
d_'8744''45''8743''45'absorptive_3342
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8743''45'isMagma_3344 ::
MAlonzo.Code.Algebra.Structures.T_IsMagma_176
d_'8743''45'isMagma_3344 :: T_IsMagma_176
d_'8743''45'isMagma_3344
= (T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_IsMagma_176)
-> Any -> Any -> T_IsMagma_176
forall a b. a -> b
coe
T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any) -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
Any
forall a. a
erased
d_'8743''45'magma_3346 :: MAlonzo.Code.Algebra.Bundles.T_Magma_68
d_'8743''45'magma_3346 :: T_Magma_68
d_'8743''45'magma_3346
= ((Any -> Any -> Any) -> T_IsMagma_176 -> T_Magma_68)
-> (Bool -> Bool -> Bool) -> T_IsMagma_176 -> T_Magma_68
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_IsMagma_176 -> T_Magma_68
MAlonzo.Code.Algebra.Bundles.C_Magma'46'constructor_1279
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24 T_IsMagma_176
d_'8743''45'isMagma_3344
d_'8743''45'isSemigroup_3348 ::
MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
d_'8743''45'isSemigroup_3348 :: T_IsSemigroup_472
d_'8743''45'isSemigroup_3348
= (T_IsMagma_176 -> (Any -> Any -> Any -> Any) -> T_IsSemigroup_472)
-> Any -> Any -> T_IsSemigroup_472
forall a b. a -> b
coe
T_IsMagma_176 -> (Any -> Any -> Any -> Any) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
(T_IsMagma_176 -> Any
forall a b. a -> b
coe T_IsMagma_176
d_'8743''45'isMagma_3344) Any
forall a. a
erased
d_'8743''45'semigroup_3350 ::
MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
d_'8743''45'semigroup_3350 :: T_Semigroup_536
d_'8743''45'semigroup_3350
= ((Any -> Any -> Any) -> T_IsSemigroup_472 -> T_Semigroup_536)
-> (Bool -> Bool -> Bool) -> T_IsSemigroup_472 -> T_Semigroup_536
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_IsSemigroup_472 -> T_Semigroup_536
MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_9793
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
T_IsSemigroup_472
d_'8743''45'isSemigroup_3348
d_'8743''45'isBand_3352 ::
MAlonzo.Code.Algebra.Structures.T_IsBand_508
d_'8743''45'isBand_3352 :: T_IsBand_508
d_'8743''45'isBand_3352
= (T_IsSemigroup_472 -> (Any -> Any) -> T_IsBand_508)
-> Any -> Any -> T_IsBand_508
forall a b. a -> b
coe
T_IsSemigroup_472 -> (Any -> Any) -> T_IsBand_508
MAlonzo.Code.Algebra.Structures.C_IsBand'46'constructor_11205
(T_IsSemigroup_472 -> Any
forall a b. a -> b
coe T_IsSemigroup_472
d_'8743''45'isSemigroup_3348) Any
forall a. a
erased
d_'8743''45'band_3354 :: MAlonzo.Code.Algebra.Bundles.T_Band_596
d_'8743''45'band_3354 :: T_Band_596
d_'8743''45'band_3354
= ((Any -> Any -> Any) -> T_IsBand_508 -> T_Band_596)
-> (Bool -> Bool -> Bool) -> T_IsBand_508 -> T_Band_596
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_IsBand_508 -> T_Band_596
MAlonzo.Code.Algebra.Bundles.C_Band'46'constructor_10881
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24 T_IsBand_508
d_'8743''45'isBand_3352
d_'8743''45'isSemilattice_3356 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeBand_590
d_'8743''45'isSemilattice_3356 :: T_IsCommutativeBand_590
d_'8743''45'isSemilattice_3356
= (T_IsBand_508 -> (Any -> Any -> Any) -> T_IsCommutativeBand_590)
-> Any -> Any -> T_IsCommutativeBand_590
forall a b. a -> b
coe
T_IsBand_508 -> (Any -> Any -> Any) -> T_IsCommutativeBand_590
MAlonzo.Code.Algebra.Structures.C_IsCommutativeBand'46'constructor_13109
(T_IsBand_508 -> Any
forall a b. a -> b
coe T_IsBand_508
d_'8743''45'isBand_3352) Any
forall a. a
erased
d_'8743''45'semilattice_3358 ::
MAlonzo.Code.Algebra.Lattice.Bundles.T_Semilattice_10
d_'8743''45'semilattice_3358 :: T_Semilattice_10
d_'8743''45'semilattice_3358
= ((Any -> Any -> Any)
-> T_IsCommutativeBand_590 -> T_Semilattice_10)
-> (Bool -> Bool -> Bool)
-> T_IsCommutativeBand_590
-> T_Semilattice_10
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_IsCommutativeBand_590 -> T_Semilattice_10
MAlonzo.Code.Algebra.Lattice.Bundles.C_Semilattice'46'constructor_193
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
T_IsCommutativeBand_590
d_'8743''45'isSemilattice_3356
d_'8743''45'isMonoid_3360 ::
MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_'8743''45'isMonoid_3360 :: T_IsMonoid_686
d_'8743''45'isMonoid_3360
= (T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686)
-> Any -> Any -> T_IsMonoid_686
forall a b. a -> b
coe
T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
(T_IsSemigroup_472 -> Any
forall a b. a -> b
coe T_IsSemigroup_472
d_'8743''45'isSemigroup_3348) (T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8743''45'identity_3260)
d_'8743''45'isCommutativeMonoid_3362 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeMonoid_736
d_'8743''45'isCommutativeMonoid_3362 :: T_IsCommutativeMonoid_736
d_'8743''45'isCommutativeMonoid_3362
= (T_IsMonoid_686
-> (Any -> Any -> Any) -> T_IsCommutativeMonoid_736)
-> Any -> Any -> T_IsCommutativeMonoid_736
forall a b. a -> b
coe
T_IsMonoid_686 -> (Any -> Any -> Any) -> T_IsCommutativeMonoid_736
MAlonzo.Code.Algebra.Structures.C_IsCommutativeMonoid'46'constructor_17695
(T_IsMonoid_686 -> Any
forall a b. a -> b
coe T_IsMonoid_686
d_'8743''45'isMonoid_3360) Any
forall a. a
erased
d_'8743''45'commutativeMonoid_3364 ::
MAlonzo.Code.Algebra.Bundles.T_CommutativeMonoid_962
d_'8743''45'commutativeMonoid_3364 :: T_CommutativeMonoid_962
d_'8743''45'commutativeMonoid_3364
= ((Any -> Any -> Any)
-> Any -> T_IsCommutativeMonoid_736 -> T_CommutativeMonoid_962)
-> (Bool -> Bool -> Bool)
-> Any
-> T_IsCommutativeMonoid_736
-> T_CommutativeMonoid_962
forall a b. a -> b
coe
(Any -> Any -> Any)
-> Any -> T_IsCommutativeMonoid_736 -> T_CommutativeMonoid_962
MAlonzo.Code.Algebra.Bundles.C_CommutativeMonoid'46'constructor_17931
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
T_IsCommutativeMonoid_736
d_'8743''45'isCommutativeMonoid_3362
d_'8743''45'isIdempotentCommutativeMonoid_3366 ::
MAlonzo.Code.Algebra.Structures.T_IsIdempotentCommutativeMonoid_852
d_'8743''45'isIdempotentCommutativeMonoid_3366 :: T_IsIdempotentCommutativeMonoid_852
d_'8743''45'isIdempotentCommutativeMonoid_3366
= (T_IsCommutativeMonoid_736
-> (Any -> Any) -> T_IsIdempotentCommutativeMonoid_852)
-> Any -> Any -> T_IsIdempotentCommutativeMonoid_852
forall a b. a -> b
coe
T_IsCommutativeMonoid_736
-> (Any -> Any) -> T_IsIdempotentCommutativeMonoid_852
MAlonzo.Code.Algebra.Structures.C_IsIdempotentCommutativeMonoid'46'constructor_20685
(T_IsCommutativeMonoid_736 -> Any
forall a b. a -> b
coe T_IsCommutativeMonoid_736
d_'8743''45'isCommutativeMonoid_3362) Any
forall a. a
erased
d_'8743''45'idempotentCommutativeMonoid_3368 ::
MAlonzo.Code.Algebra.Bundles.T_IdempotentCommutativeMonoid_1148
d_'8743''45'idempotentCommutativeMonoid_3368 :: T_IdempotentCommutativeMonoid_1148
d_'8743''45'idempotentCommutativeMonoid_3368
= ((Any -> Any -> Any)
-> Any
-> T_IsIdempotentCommutativeMonoid_852
-> T_IdempotentCommutativeMonoid_1148)
-> (Bool -> Bool -> Bool)
-> Any
-> T_IsIdempotentCommutativeMonoid_852
-> T_IdempotentCommutativeMonoid_1148
forall a b. a -> b
coe
(Any -> Any -> Any)
-> Any
-> T_IsIdempotentCommutativeMonoid_852
-> T_IdempotentCommutativeMonoid_1148
MAlonzo.Code.Algebra.Bundles.C_IdempotentCommutativeMonoid'46'constructor_21499
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
T_IsIdempotentCommutativeMonoid_852
d_'8743''45'isIdempotentCommutativeMonoid_3366
d_'8744''45''8743''45'isSemiring_3370 ::
MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570
d_'8744''45''8743''45'isSemiring_3370 :: T_IsSemiring_1570
d_'8744''45''8743''45'isSemiring_3370
= (T_IsSemiringWithoutAnnihilatingZero_1468
-> T_Σ_14 -> T_IsSemiring_1570)
-> Any -> Any -> T_IsSemiring_1570
forall a b. a -> b
coe
T_IsSemiringWithoutAnnihilatingZero_1468
-> T_Σ_14 -> T_IsSemiring_1570
MAlonzo.Code.Algebra.Structures.C_IsSemiring'46'constructor_48071
((T_IsCommutativeMonoid_736
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_Σ_14
-> T_IsSemiringWithoutAnnihilatingZero_1468)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsCommutativeMonoid_736
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_Σ_14
-> T_IsSemiringWithoutAnnihilatingZero_1468
MAlonzo.Code.Algebra.Structures.C_IsSemiringWithoutAnnihilatingZero'46'constructor_43811
(T_IsCommutativeMonoid_736 -> Any
forall a b. a -> b
coe T_IsCommutativeMonoid_736
d_'8744''45'isCommutativeMonoid_3236) Any
forall a. a
erased Any
forall a. a
erased
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8743''45'identity_3260)
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8743''45'distrib'45''8744'_3308))
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8743''45'zero_3266)
d_'8744''45''8743''45'isCommutativeSemiring_3372 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678
d_'8744''45''8743''45'isCommutativeSemiring_3372 :: T_IsCommutativeSemiring_1678
d_'8744''45''8743''45'isCommutativeSemiring_3372
= (T_IsSemiring_1570
-> (Any -> Any -> Any) -> T_IsCommutativeSemiring_1678)
-> Any -> Any -> T_IsCommutativeSemiring_1678
forall a b. a -> b
coe
T_IsSemiring_1570
-> (Any -> Any -> Any) -> T_IsCommutativeSemiring_1678
MAlonzo.Code.Algebra.Structures.C_IsCommutativeSemiring'46'constructor_51895
(T_IsSemiring_1570 -> Any
forall a b. a -> b
coe T_IsSemiring_1570
d_'8744''45''8743''45'isSemiring_3370) Any
forall a. a
erased
d_'8744''45''8743''45'commutativeSemiring_3374 ::
MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2446
d_'8744''45''8743''45'commutativeSemiring_3374 :: T_CommutativeSemiring_2446
d_'8744''45''8743''45'commutativeSemiring_3374
= ((Any -> Any -> Any)
-> (Any -> Any -> Any)
-> Any
-> Any
-> T_IsCommutativeSemiring_1678
-> T_CommutativeSemiring_2446)
-> (Bool -> Bool -> Bool)
-> (Bool -> Bool -> Bool)
-> Any
-> Any
-> T_IsCommutativeSemiring_1678
-> T_CommutativeSemiring_2446
forall a b. a -> b
coe
(Any -> Any -> Any)
-> (Any -> Any -> Any)
-> Any
-> Any
-> T_IsCommutativeSemiring_1678
-> T_CommutativeSemiring_2446
MAlonzo.Code.Algebra.Bundles.C_CommutativeSemiring'46'constructor_44731
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
T_IsCommutativeSemiring_1678
d_'8744''45''8743''45'isCommutativeSemiring_3372
d_'8743''45''8744''45'isSemiring_3376 ::
MAlonzo.Code.Algebra.Structures.T_IsSemiring_1570
d_'8743''45''8744''45'isSemiring_3376 :: T_IsSemiring_1570
d_'8743''45''8744''45'isSemiring_3376
= (T_IsSemiringWithoutAnnihilatingZero_1468
-> T_Σ_14 -> T_IsSemiring_1570)
-> Any -> Any -> T_IsSemiring_1570
forall a b. a -> b
coe
T_IsSemiringWithoutAnnihilatingZero_1468
-> T_Σ_14 -> T_IsSemiring_1570
MAlonzo.Code.Algebra.Structures.C_IsSemiring'46'constructor_48071
((T_IsCommutativeMonoid_736
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_Σ_14
-> T_IsSemiringWithoutAnnihilatingZero_1468)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_IsCommutativeMonoid_736
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_Σ_14
-> T_IsSemiringWithoutAnnihilatingZero_1468
MAlonzo.Code.Algebra.Structures.C_IsSemiringWithoutAnnihilatingZero'46'constructor_43811
(T_IsCommutativeMonoid_736 -> Any
forall a b. a -> b
coe T_IsCommutativeMonoid_736
d_'8743''45'isCommutativeMonoid_3362) Any
forall a. a
erased Any
forall a. a
erased
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8744''45'identity_3188)
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8744''45'distrib'45''8743'_3328))
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8744''45'zero_3194)
d_'8743''45''8744''45'isCommutativeSemiring_3378 ::
MAlonzo.Code.Algebra.Structures.T_IsCommutativeSemiring_1678
d_'8743''45''8744''45'isCommutativeSemiring_3378 :: T_IsCommutativeSemiring_1678
d_'8743''45''8744''45'isCommutativeSemiring_3378
= (T_IsSemiring_1570
-> (Any -> Any -> Any) -> T_IsCommutativeSemiring_1678)
-> Any -> Any -> T_IsCommutativeSemiring_1678
forall a b. a -> b
coe
T_IsSemiring_1570
-> (Any -> Any -> Any) -> T_IsCommutativeSemiring_1678
MAlonzo.Code.Algebra.Structures.C_IsCommutativeSemiring'46'constructor_51895
(T_IsSemiring_1570 -> Any
forall a b. a -> b
coe T_IsSemiring_1570
d_'8743''45''8744''45'isSemiring_3376) Any
forall a. a
erased
d_'8743''45''8744''45'commutativeSemiring_3380 ::
MAlonzo.Code.Algebra.Bundles.T_CommutativeSemiring_2446
d_'8743''45''8744''45'commutativeSemiring_3380 :: T_CommutativeSemiring_2446
d_'8743''45''8744''45'commutativeSemiring_3380
= ((Any -> Any -> Any)
-> (Any -> Any -> Any)
-> Any
-> Any
-> T_IsCommutativeSemiring_1678
-> T_CommutativeSemiring_2446)
-> (Bool -> Bool -> Bool)
-> (Bool -> Bool -> Bool)
-> Any
-> Any
-> T_IsCommutativeSemiring_1678
-> T_CommutativeSemiring_2446
forall a b. a -> b
coe
(Any -> Any -> Any)
-> (Any -> Any -> Any)
-> Any
-> Any
-> T_IsCommutativeSemiring_1678
-> T_CommutativeSemiring_2446
MAlonzo.Code.Algebra.Bundles.C_CommutativeSemiring'46'constructor_44731
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
T_IsCommutativeSemiring_1678
d_'8743''45''8744''45'isCommutativeSemiring_3378
d_'8744''45''8743''45'isLattice_3382 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsLattice_2962
d_'8744''45''8743''45'isLattice_3382 :: T_IsLattice_2962
d_'8744''45''8743''45'isLattice_3382
= (T_IsEquivalence_26
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_IsLattice_2962)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> T_IsLattice_2962
forall a b. a -> b
coe
T_IsEquivalence_26
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
-> T_Σ_14
-> T_IsLattice_2962
MAlonzo.Code.Algebra.Lattice.Structures.C_IsLattice'46'constructor_36793
(T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
Any
forall a. a
erased Any
forall a. a
erased Any
forall a. a
erased Any
forall a. a
erased Any
forall a. a
erased Any
forall a. a
erased
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8744''45''8743''45'absorptive_3342)
d_'8744''45''8743''45'lattice_3384 ::
MAlonzo.Code.Algebra.Lattice.Bundles.T_Lattice_500
d_'8744''45''8743''45'lattice_3384 :: T_Lattice_500
d_'8744''45''8743''45'lattice_3384
= ((Any -> Any -> Any)
-> (Any -> Any -> Any) -> T_IsLattice_2962 -> T_Lattice_500)
-> (Bool -> Bool -> Bool)
-> (Bool -> Bool -> Bool)
-> T_IsLattice_2962
-> T_Lattice_500
forall a b. a -> b
coe
(Any -> Any -> Any)
-> (Any -> Any -> Any) -> T_IsLattice_2962 -> T_Lattice_500
MAlonzo.Code.Algebra.Lattice.Bundles.C_Lattice'46'constructor_7925
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
T_IsLattice_2962
d_'8744''45''8743''45'isLattice_3382
d_'8744''45''8743''45'isDistributiveLattice_3386 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsDistributiveLattice_3036
d_'8744''45''8743''45'isDistributiveLattice_3386 :: T_IsDistributiveLattice_3036
d_'8744''45''8743''45'isDistributiveLattice_3386
= (T_IsLattice_2962
-> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3036)
-> Any -> Any -> Any -> T_IsDistributiveLattice_3036
forall a b. a -> b
coe
T_IsLattice_2962
-> T_Σ_14 -> T_Σ_14 -> T_IsDistributiveLattice_3036
MAlonzo.Code.Algebra.Lattice.Structures.C_IsDistributiveLattice'46'constructor_40943
(T_IsLattice_2962 -> Any
forall a b. a -> b
coe T_IsLattice_2962
d_'8744''45''8743''45'isLattice_3382)
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8744''45'distrib'45''8743'_3328)
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8743''45'distrib'45''8744'_3308)
d_'8744''45''8743''45'distributiveLattice_3388 ::
MAlonzo.Code.Algebra.Lattice.Bundles.T_DistributiveLattice_584
d_'8744''45''8743''45'distributiveLattice_3388 :: T_DistributiveLattice_584
d_'8744''45''8743''45'distributiveLattice_3388
= ((Any -> Any -> Any)
-> (Any -> Any -> Any)
-> T_IsDistributiveLattice_3036
-> T_DistributiveLattice_584)
-> (Bool -> Bool -> Bool)
-> (Bool -> Bool -> Bool)
-> T_IsDistributiveLattice_3036
-> T_DistributiveLattice_584
forall a b. a -> b
coe
(Any -> Any -> Any)
-> (Any -> Any -> Any)
-> T_IsDistributiveLattice_3036
-> T_DistributiveLattice_584
MAlonzo.Code.Algebra.Lattice.Bundles.C_DistributiveLattice'46'constructor_9515
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
T_IsDistributiveLattice_3036
d_'8744''45''8743''45'isDistributiveLattice_3386
d_'8744''45''8743''45'isBooleanAlgebra_3390 ::
MAlonzo.Code.Algebra.Lattice.Structures.T_IsBooleanAlgebra_3112
d_'8744''45''8743''45'isBooleanAlgebra_3390 :: T_IsBooleanAlgebra_3112
d_'8744''45''8743''45'isBooleanAlgebra_3390
= (T_IsDistributiveLattice_3036
-> T_Σ_14
-> T_Σ_14
-> (Any -> Any -> Any -> Any)
-> T_IsBooleanAlgebra_3112)
-> Any -> Any -> Any -> Any -> T_IsBooleanAlgebra_3112
forall a b. a -> b
coe
T_IsDistributiveLattice_3036
-> T_Σ_14
-> T_Σ_14
-> (Any -> Any -> Any -> Any)
-> T_IsBooleanAlgebra_3112
MAlonzo.Code.Algebra.Lattice.Structures.C_IsBooleanAlgebra'46'constructor_44015
(T_IsDistributiveLattice_3036 -> Any
forall a b. a -> b
coe T_IsDistributiveLattice_3036
d_'8744''45''8743''45'isDistributiveLattice_3386)
(T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8744''45'inverse_3202) (T_Σ_14 -> Any
forall a b. a -> b
coe T_Σ_14
d_'8743''45'inverse_3274)
Any
forall a. a
erased
d_'8744''45''8743''45'booleanAlgebra_3392 ::
MAlonzo.Code.Algebra.Lattice.Bundles.T_BooleanAlgebra_682
d_'8744''45''8743''45'booleanAlgebra_3392 :: T_BooleanAlgebra_682
d_'8744''45''8743''45'booleanAlgebra_3392
= ((Any -> Any -> Any)
-> (Any -> Any -> Any)
-> (Any -> Any)
-> Any
-> Any
-> T_IsBooleanAlgebra_3112
-> T_BooleanAlgebra_682)
-> (Bool -> Bool -> Bool)
-> (Bool -> Bool -> Bool)
-> (Bool -> Bool)
-> Any
-> Any
-> T_IsBooleanAlgebra_3112
-> T_BooleanAlgebra_682
forall a b. a -> b
coe
(Any -> Any -> Any)
-> (Any -> Any -> Any)
-> (Any -> Any)
-> Any
-> Any
-> T_IsBooleanAlgebra_3112
-> T_BooleanAlgebra_682
MAlonzo.Code.Algebra.Lattice.Bundles.C_BooleanAlgebra'46'constructor_11509
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
T_IsBooleanAlgebra_3112
d_'8744''45''8743''45'isBooleanAlgebra_3390
d_not'45'involutive_3394 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_not'45'involutive_3394 :: Bool -> T__'8801'__12
d_not'45'involutive_3394 = Bool -> T__'8801'__12
forall a. a
erased
d_not'45'injective_3400 ::
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_not'45'injective_3400 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
d_not'45'injective_3400 = Bool -> Bool -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
d_not'45''172'_3410 ::
Bool ->
Bool ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_not'45''172'_3410 :: Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 -> T_Irrelevant_20
d_not'45''172'_3410 = Bool -> Bool -> T__'8801'__12 -> T__'8801'__12 -> T_Irrelevant_20
forall a. a
erased
d_'172''45'not_3416 ::
Bool ->
Bool ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'172''45'not_3416 :: Bool -> Bool -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8801'__12
d_'172''45'not_3416 = Bool -> Bool -> (T__'8801'__12 -> T_Irrelevant_20) -> T__'8801'__12
forall a. a
erased
d_xor'45'is'45'ok_3426 ::
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_xor'45'is'45'ok_3426 :: Bool -> Bool -> T__'8801'__12
d_xor'45'is'45'ok_3426 = Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_true'45'xor_3434 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_true'45'xor_3434 :: Bool -> T__'8801'__12
d_true'45'xor_3434 = Bool -> T__'8801'__12
forall a. a
erased
d_xor'45'same_3438 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_xor'45'same_3438 :: Bool -> T__'8801'__12
d_xor'45'same_3438 = Bool -> T__'8801'__12
forall a. a
erased
d_not'45'distrib'737''45'xor_3444 ::
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_not'45'distrib'737''45'xor_3444 :: Bool -> Bool -> T__'8801'__12
d_not'45'distrib'737''45'xor_3444 = Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_not'45'distrib'691''45'xor_3454 ::
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_not'45'distrib'691''45'xor_3454 :: Bool -> Bool -> T__'8801'__12
d_not'45'distrib'691''45'xor_3454 = Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_xor'45'assoc_3460 ::
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_xor'45'assoc_3460 :: Bool -> Bool -> Bool -> T__'8801'__12
d_xor'45'assoc_3460 = Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_xor'45'comm_3470 ::
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_xor'45'comm_3470 :: Bool -> Bool -> T__'8801'__12
d_xor'45'comm_3470 = Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_xor'45'identity'737'_3472 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_xor'45'identity'737'_3472 :: Bool -> T__'8801'__12
d_xor'45'identity'737'_3472 = Bool -> T__'8801'__12
forall a. a
erased
d_xor'45'identity'691'_3474 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_xor'45'identity'691'_3474 :: Bool -> T__'8801'__12
d_xor'45'identity'691'_3474 = Bool -> T__'8801'__12
forall a. a
erased
d_xor'45'identity_3476 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_xor'45'identity_3476 :: T_Σ_14
d_xor'45'identity_3476
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_xor'45'inverse'737'_3478 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_xor'45'inverse'737'_3478 :: Bool -> T__'8801'__12
d_xor'45'inverse'737'_3478 = Bool -> T__'8801'__12
forall a. a
erased
d_xor'45'inverse'691'_3480 ::
Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_xor'45'inverse'691'_3480 :: Bool -> T__'8801'__12
d_xor'45'inverse'691'_3480 = Bool -> T__'8801'__12
forall a. a
erased
d_xor'45'inverse_3484 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_xor'45'inverse_3484 :: T_Σ_14
d_xor'45'inverse_3484
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_'8743''45'distrib'737''45'xor_3486 ::
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'distrib'737''45'xor_3486 :: Bool -> Bool -> Bool -> T__'8801'__12
d_'8743''45'distrib'737''45'xor_3486 = Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'distrib'691''45'xor_3496 ::
Bool ->
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8743''45'distrib'691''45'xor_3496 :: Bool -> Bool -> Bool -> T__'8801'__12
d_'8743''45'distrib'691''45'xor_3496 = Bool -> Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_'8743''45'distrib'45'xor_3506 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8743''45'distrib'45'xor_3506 :: T_Σ_14
d_'8743''45'distrib'45'xor_3506
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased
d_xor'45'annihilates'45'not_3512 ::
Bool -> Bool -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_xor'45'annihilates'45'not_3512 :: Bool -> Bool -> T__'8801'__12
d_xor'45'annihilates'45'not_3512 = Bool -> Bool -> T__'8801'__12
forall a. a
erased
d_xor'45''8743''45'commutativeRing_3518 ::
MAlonzo.Code.Algebra.Bundles.T_CommutativeRing_4016
d_xor'45''8743''45'commutativeRing_3518 :: T_CommutativeRing_4016
d_xor'45''8743''45'commutativeRing_3518
= (T_BooleanAlgebra_682
-> (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> T_CommutativeRing_4016)
-> Any -> Any -> Any -> T_CommutativeRing_4016
forall a b. a -> b
coe
T_BooleanAlgebra_682
-> (Any -> Any -> Any)
-> (Any -> Any -> Any)
-> T_CommutativeRing_4016
MAlonzo.Code.Algebra.Lattice.Properties.BooleanAlgebra.du_'8853''45''8743''45'commutativeRing_3706
(T_BooleanAlgebra_682 -> Any
forall a b. a -> b
coe T_BooleanAlgebra_682
d_'8744''45''8743''45'booleanAlgebra_3392)
((Bool -> Bool -> Bool) -> Any
forall a b. a -> b
coe Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__xor__36) Any
forall a. a
erased
d_if'45'float_3792 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
Bool ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_if'45'float_3792 :: ()
-> ()
-> ()
-> ()
-> (Any -> Any)
-> Bool
-> Any
-> Any
-> T__'8801'__12
d_if'45'float_3792 = ()
-> ()
-> ()
-> ()
-> (Any -> Any)
-> Bool
-> Any
-> Any
-> T__'8801'__12
forall a. a
erased
d_T'45''8801'_3796 ::
Bool -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_T'45''8801'_3796 :: Bool -> T_Equivalence_1714
d_T'45''8801'_3796 Bool
v0
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 Any
forall a. a
erased
(let v1 :: b
v1 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
Any -> Any
forall a b. a -> b
coe ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 -> Any
forall a. a
v1)))
else ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 Any
forall a. a
erased Any
forall a. a
erased
d_T'45'not'45''8801'_3800 ::
Bool -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_T'45'not'45''8801'_3800 :: Bool -> T_Equivalence_1714
d_T'45'not'45''8801'_3800 Bool
v0
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 Any
forall a. a
erased Any
forall a. a
erased
else ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 Any
forall a. a
erased
(let v1 :: b
v1 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
Any -> Any
forall a b. a -> b
coe ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 -> Any
forall a. a
v1)))
d_T'45''8743'_3806 ::
Bool -> Bool -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_T'45''8743'_3806 :: Bool -> Bool -> T_Equivalence_1714
d_T'45''8743'_3806 Bool
v0 Bool
v1
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
(let v2 :: t
v2
= (Any -> Any -> T_Σ_14) -> Any -> Any -> t
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
(() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8) in
Any -> Any
forall a b. a -> b
coe ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v3 -> Any
forall a. a
v2)))
(let v2 :: b
v2 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
Any -> Any
forall a b. a -> b
coe ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v3 -> Any
forall a. a
v2)))
else ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v2)))
else ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v2)))
d_T'45''8744'_3812 ::
Bool -> Bool -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_T'45''8744'_3812 :: Bool -> Bool -> T_Equivalence_1714
d_T'45''8744'_3812 Bool
v0 Bool
v1
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
(let v2 :: b
v2 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
Any -> Any
forall a b. a -> b
coe ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v3 -> Any
forall a. a
v2)))
else (if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
(let v2 :: b
v2 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
Any -> Any
forall a b. a -> b
coe ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v3 -> Any
forall a. a
v2)))
else ((Any -> Any) -> (Any -> Any) -> T_Equivalence_1714)
-> Any -> Any -> T_Equivalence_1714
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298
((Any -> T__'8846'__30) -> Any
forall a b. a -> b
coe Any -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
(((Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T__'8846'__30 -> Any
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52 ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 -> Any
v2))
((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 -> Any
v2))))
d_T'45'irrelevant_3814 ::
Bool ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_T'45'irrelevant_3814 :: Bool -> Any -> Any -> T__'8801'__12
d_T'45'irrelevant_3814 = Bool -> Any -> Any -> T__'8801'__12
forall a. a
erased
d_T'63''45'diag_3818 :: Bool -> AgdaAny -> AgdaAny
d_T'63''45'diag_3818 :: Bool -> Any -> Any
d_T'63''45'diag_3818 Bool
v0
= (T_Dec_20 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> Any -> Any
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_fromWitness_140
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v0)
((Bool -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66
(Bool -> Any
forall a b. a -> b
coe Bool
v0)))
d_'8660''8594''8801'_3828 ::
Bool ->
Bool ->
Bool ->
MAlonzo.Code.Function.Bundles.T_Equivalence_1714 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8660''8594''8801'_3828 :: Bool -> Bool -> Bool -> T_Equivalence_1714 -> T__'8801'__12
d_'8660''8594''8801'_3828 = Bool -> Bool -> Bool -> T_Equivalence_1714 -> T__'8801'__12
forall a. a
erased
d_push'45'function'45'into'45'if_3842 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
Bool ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_push'45'function'45'into'45'if_3842 :: ()
-> ()
-> ()
-> ()
-> (Any -> Any)
-> Bool
-> Any
-> Any
-> T__'8801'__12
d_push'45'function'45'into'45'if_3842 = ()
-> ()
-> ()
-> ()
-> (Any -> Any)
-> Bool
-> Any
-> Any
-> T__'8801'__12
forall a. a
erased