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

MAlonzo.Code.Algebra.Structures.Biased

Documentation

d__DistributesOver__18T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d__DistributesOver'691'__20T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d__DistributesOver'737'__22T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Commutative_42T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftIdentity_84T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_LeftZero_92T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightIdentity_114T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_RightZero_122T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Zero_142T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → AgdaAny → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_IsAbelianGroup_146 ∷ p → p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid_158 ∷ p → p → p → p → p → p → () Source #

d_IsCommutativeSemiring_164 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsMonoid_196 ∷ p → p → p → p → p → p → () Source #

d_IsNearSemiring_200 ∷ p → p → p → p → p → p → p → () Source #

d_IsRing_212 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_IsSemigroup_218 ∷ p → p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_224 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutOne_226 ∷ p → p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid'737'_2662 ∷ p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid'691'_2716 ∷ p → p → p → p → p → p → () Source #

d_IsSemiringWithoutOne'42'_2772 ∷ p → p → p → p → p → p → p → () Source #

d_IsNearSemiring'42'_2834 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero'42'_2898 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCommutativeSemiring'737'_2970 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCommutativeSemiring'691'_3098 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsRing'42'_3228 ∷ p → p → p → p → p → p → p → p → p → () Source #

d_isRing_3256T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing'42'_3228T_IsRing_2650 Source #

d_identity'691'_3268T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing'42'_3228AgdaAnyAgdaAny Source #

d_identity'737'_3270T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing'42'_3228AgdaAnyAgdaAny Source #

d_reflexive_3284T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing'42'_3228AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_setoid_3286T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing'42'_3228T_Setoid_44 Source #

d_IsRingWithoutAnnihilatingZero_3308 ∷ p → p → p → p → p → p → p → p → p → () Source #