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

MAlonzo.Code.Algebra.Structures

Documentation

d_Alternative_34 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Associative_36 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Commutative_40 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Congruent'8321'_42 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> () #

d_Congruent'8322'_44 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Flexible_48 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Idempotent_50 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Identical_54 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Identity_56 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Inverse_60 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftAlternative_66 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftBol_68 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftCongruent_72 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftDivides_76 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftIdentity_82 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftInverse_84 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftSemimedial_88 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_LeftZero_90 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Medial_92 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_MiddleBol_94 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightBol_98 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightCongruent_102 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightDivides_106 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightIdentity_112 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightInverse_114 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_RightZero_120 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Selective_122 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_Semimedial_126 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_StarDestructive_128 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_StarExpansive_130 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> () #

d_Zero_140 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> () #

d_IsSuccessorSet_146 :: p -> p -> p -> p -> p -> p -> () #

d_IsMagma_176 :: p -> p -> p -> p -> p -> () #

d_IsCommutativeMagma_212 :: p -> p -> p -> p -> p -> () #

d_IsIdempotentMagma_248 :: p -> p -> p -> p -> p -> () #

d_IsAlternativeMagma_284 :: p -> p -> p -> p -> p -> () #

d_IsFlexibleMagma_324 :: p -> p -> p -> p -> p -> () #

d_IsMedialMagma_360 :: p -> p -> p -> p -> p -> () #

d_IsSemimedialMagma_396 :: p -> p -> p -> p -> p -> () #

d_IsSelectiveMagma_436 :: p -> p -> p -> p -> p -> () #

d_IsSemigroup_472 :: p -> p -> p -> p -> p -> () #

d_IsBand_508 :: p -> p -> p -> p -> p -> () #

d_IsCommutativeSemigroup_548 :: p -> p -> p -> p -> p -> () #

d_IsCommutativeBand_590 :: p -> p -> p -> p -> p -> () #

d_IsUnitalMagma_642 :: p -> p -> p -> p -> p -> p -> () #

d_IsMonoid_686 :: p -> p -> p -> p -> p -> p -> () #

d_IsCommutativeMonoid_736 :: p -> p -> p -> p -> p -> p -> () #

d_IsIdempotentMonoid_796 :: p -> p -> p -> p -> p -> p -> () #

d_IsIdempotentCommutativeMonoid_852 :: p -> p -> p -> p -> p -> p -> () #

d_IsInvertibleMagma_924 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsInvertibleUnitalMagma_976 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsGroup_1036 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsAbelianGroup_1132 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsNearSemiring_1218 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsSemiringWithoutOne_1298 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsCommutativeSemiringWithoutOne_1382 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsSemiringWithoutAnnihilatingZero_1468 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsSemiring_1570 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsCommutativeSemiring_1678 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsCancellativeCommutativeSemiring_1798 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsIdempotentSemiring_1922 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsKleeneAlgebra_2044 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsQuasiring_2180 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsRingWithoutOne_2286 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsNonAssociativeRing_2408 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsNearring_2538 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsRing_2650 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsCommutativeRing_2796 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsQuasigroup_2944 :: p -> p -> p -> p -> p -> p -> p -> () #

d_IsLoop_3026 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsLeftBolLoop_3104 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsRightBolLoop_3186 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsMoufangLoop_3268 :: p -> p -> p -> p -> p -> p -> p -> p -> () #

d_IsMiddleBolLoop_3358 :: p -> p -> p -> p -> p -> p -> p -> p -> () #