plutus-metatheory-1.72.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Algebra.Structures

Documentation

d__DistributesOver__16 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'691'__18 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__20 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_AlmostLeftCancellative_30 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_AlmostRightCancellative_32 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Alternative_34 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Associative_36 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Commutative_40 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Congruent'8321'_42 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → () Source #

d_Congruent'8322'_44 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Flexible_48 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Idempotent_50 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Identical_54 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Identity_56 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Inverse_60 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftAlternative_66 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftBol_68 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftCongruent_72 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftDivides_76 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftDivides'691'_78 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftDivides'737'_80 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftIdentity_82 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftInverse_84 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftSemimedial_88 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftZero_90 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Medial_92 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_MiddleBol_94 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightAlternative_96 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightBol_98 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightCongruent_102 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightDivides_106 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightDivides'691'_108 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightDivides'737'_110 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightIdentity_112 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightInverse_114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightSemimedial_118 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightZero_120 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Selective_122 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Semimedial_126 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_StarDestructive_128 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarExpansive_130 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarLeftDestructive_132 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarLeftExpansive_134 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarRightDestructive_136 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_StarRightExpansive_138 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #

d_Zero_140 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_IsSuccessorSet_146 ∷ p → p → p → p → p → p → () Source #

d_IsMagma_178 ∷ p → p → p → p → p → () Source #

d_IsCommutativeMagma_214 ∷ p → p → p → p → p → () Source #

d_IsIdempotentMagma_252 ∷ p → p → p → p → p → () Source #

d_IsAlternativeMagma_290 ∷ p → p → p → p → p → () Source #

d_IsFlexibleMagma_332 ∷ p → p → p → p → p → () Source #

d_IsMedialMagma_370 ∷ p → p → p → p → p → () Source #

d_IsSemimedialMagma_408 ∷ p → p → p → p → p → () Source #

d_IsSelectiveMagma_450 ∷ p → p → p → p → p → () Source #

d_IsSemigroup_488 ∷ p → p → p → p → p → () Source #

d_IsBand_526 ∷ p → p → p → p → p → () Source #

d_setoid_552 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → T_Setoid_46 Source #

d_IsCommutativeSemigroup_568 ∷ p → p → p → p → p → () Source #

d_IsCommutativeBand_612 ∷ p → p → p → p → p → () Source #

d_IsUnitalMagma_666 ∷ p → p → p → p → p → p → () Source #

d_IsMonoid_712 ∷ p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid_764 ∷ p → p → p → p → p → p → () Source #

d_IsIdempotentMonoid_826 ∷ p → p → p → p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_884 ∷ p → p → p → p → p → p → () Source #

d_IsInvertibleMagma_958 ∷ p → p → p → p → p → p → p → () Source #

d_IsInvertibleUnitalMagma_1012 ∷ p → p → p → p → p → p → p → () Source #

d_IsGroup_1074 ∷ p → p → p → p → p → p → p → () Source #

d_setoid_1118 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1074 → T_Setoid_46 Source #

d__'92''92'__1130 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1074 → AgdaAny → AgdaAny → AgdaAny Source #

d__'47''47'__1136 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1074 → AgdaAny → AgdaAny → AgdaAny Source #

d__'45'__1142 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1074 → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse'737'_1144 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1074 → AgdaAny → AgdaAny Source #

d_inverse'691'_1146 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_IsGroup_1074 → AgdaAny → AgdaAny Source #

d_IsAbelianGroup_1172 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiring_1260 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutOne_1342 ∷ p → p → p → p → p → p → p → () Source #

d_IsCommutativeSemiringWithoutOne_1438 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_1536 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSemiring_1640 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_1724 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1640 → T_Setoid_46 Source #

d_zero'691'_1736 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1640 → AgdaAny → AgdaAny Source #

d_zero'737'_1738 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsSemiring_1640 → AgdaAny → AgdaAny Source #

d_IsCommutativeSemiring_1750 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCancellativeCommutativeSemiring_1872 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsIdempotentSemiring_1998 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsKleeneAlgebra_2122 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_zero'691'_2238 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsKleeneAlgebra_2122 → AgdaAny → AgdaAny Source #

d_zero'737'_2240 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsKleeneAlgebra_2122 → AgdaAny → AgdaAny Source #

d_IsQuasiring_2260 ∷ p → p → p → p → p → p → p → p → () Source #

d_zero'737'_2334 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsQuasiring_2260 → AgdaAny → AgdaAny Source #

d_zero'691'_2336 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsQuasiring_2260 → AgdaAny → AgdaAny Source #

d_IsRingWithoutOne_2368 ∷ p → p → p → p → p → p → p → p → () Source #

d_zero_2468 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutOne_2368 → T_Σ_14 Source #

d_IsNonAssociativeRing_2494 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_IsNearring_2626 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_identity'691'_2662 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny Source #

d_identity'737'_2664 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny Source #

d_identity'691'_2682 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny Source #

d_identity'737'_2684 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny Source #

d_distrib'691'_2696 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'737'_2698 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity'691'_2700 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny Source #

d_identity'737'_2702 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny Source #

d_reflexive_2710 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2712 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → T_Setoid_46 Source #

d_zero'691'_2720 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny Source #

d_zero'737'_2722 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T_IsNearring_2626 → AgdaAny → AgdaAny Source #

d_IsRing_2740 ∷ p → p → p → p → p → p → p → p → p → () Source #

d__'47''47'__2776 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2778 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2780 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc_2786 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2788 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong_2790 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_2792 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_2794 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity_2796 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → T_Σ_14 Source #

d_identity'691'_2798 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny Source #

d_identity'737'_2800 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny Source #

d_isGroup_2808 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → T_IsGroup_1074 Source #

d_isMagma_2814 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → T_IsMagma_178 Source #

d_isMonoid_2816 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → T_IsMonoid_712 Source #

d_'8315''185''45'cong_2822 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse_2824 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → T_Σ_14 Source #

d_inverse'691'_2826 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny Source #

d_inverse'737'_2828 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny Source #

d_distrib'691'_2830 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'737'_2832 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_refl_2840 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny Source #

d_reflexive_2842 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_setoid_2844 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → T_Setoid_46 Source #

d_sym_2846 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_2848 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero_2854 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → T_Σ_14 Source #

d_zero'691'_2856 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny Source #

d_zero'737'_2858 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny Source #

d_identity'691'_2864 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny Source #

d_identity'737'_2866 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRing_2740 → AgdaAny → AgdaAny Source #

d_IsCommutativeRing_2888 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_assoc_2932 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_2888 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm_2934 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_2888 → AgdaAny → AgdaAny → AgdaAny Source #

d_inverse_2972 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_2888 → T_Σ_14 Source #

d_refl_2998 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_2888 → AgdaAny → AgdaAny Source #

d_sym_3004 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_2888 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_trans_3006 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_2888 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_zero_3012 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeRing_2888 → T_Σ_14 Source #

d_IsQuasigroup_3038 ∷ p → p → p → p → p → p → p → () Source #

d_setoid_3076 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsQuasigroup_3038 → T_Setoid_46 Source #

d_IsLoop_3122 ∷ p → p → p → p → p → p → p → p → () Source #

d_leftDivides'691'_3162 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → AgdaAny → AgdaAny → AgdaAny Source #

d_leftDivides'737'_3164 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → AgdaAny → AgdaAny → AgdaAny Source #

d_reflexive_3168 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #

d_rightDivides'691'_3172 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → AgdaAny → AgdaAny → AgdaAny Source #

d_rightDivides'737'_3174 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → AgdaAny → AgdaAny → AgdaAny Source #

d_setoid_3176 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → T_Setoid_46 Source #

d_'8729''45'cong'691'_3184 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_3186 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_identity'737'_3188 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → AgdaAny → AgdaAny Source #

d_identity'691'_3190 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLoop_3122 → AgdaAny → AgdaAny Source #

d_IsLeftBolLoop_3202 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_3264 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsLeftBolLoop_3202 → T_Setoid_46 Source #

d_IsRightBolLoop_3286 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_3348 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsRightBolLoop_3286 → T_Setoid_46 Source #

d_IsMoufangLoop_3370 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_3440 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsMoufangLoop_3370 → T_Setoid_46 Source #

d_IsMiddleBolLoop_3462 ∷ p → p → p → p → p → p → p → p → () Source #