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

MAlonzo.Code.Algebra.Structures

Documentation

d__Absorbs__14T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d__DistributesOver__16T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

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

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

d_Absorptive_24T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

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

d_Associative_32T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Commutative_36T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Congruent'8321'_38T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAny) → () Source #

d_Congruent'8322'_40T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

d_Idempotent_44T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

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

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

d_LeftCongruent_58T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

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

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

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

d_RightCongruent_70T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

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

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

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

d_Selective_80T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → () Source #

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

d_IsMagma_86 ∷ p → p → p → p → p → () Source #

d_setoid_110T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → T_IsMagma_86T_Setoid_44 Source #

d_IsCommutativeMagma_122 ∷ p → p → p → p → p → () Source #

d_IsSelectiveMagma_158 ∷ p → p → p → p → p → () Source #

d_IsSemigroup_194 ∷ p → p → p → p → p → () Source #

d_IsBand_230 ∷ p → p → p → p → p → () Source #

d_setoid_256T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → T_IsBand_230T_Setoid_44 Source #

d_IsCommutativeSemigroup_270 ∷ p → p → p → p → p → () Source #

d_IsSemilattice_312 ∷ p → p → p → p → p → () Source #

d_IsMonoid_358 ∷ p → p → p → p → p → p → () Source #

d_IsCommutativeMonoid_406 ∷ p → p → p → p → p → p → () Source #

d_IsIdempotentCommutativeMonoid_464 ∷ p → p → p → p → p → p → () Source #

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

d_IsGroup_580 ∷ p → p → p → p → p → p → p → () Source #

d_identity'691'_606T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_580AgdaAnyAgdaAny Source #

d_identity'737'_608T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_580AgdaAnyAgdaAny Source #

d_reflexive_620T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_580AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_setoid_622T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_580T_Setoid_44 Source #

d__'45'__634T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_580AgdaAnyAgdaAnyAgdaAny Source #

d_inverse'737'_640T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_580AgdaAnyAgdaAny Source #

d_inverse'691'_642T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsGroup_580AgdaAnyAgdaAny Source #

d_IsAbelianGroup_662 ∷ p → p → p → p → p → p → p → () Source #

d__'45'__680T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAny → (AgdaAnyAgdaAny) → T_IsAbelianGroup_662AgdaAnyAgdaAnyAgdaAny Source #

d_IsLattice_740 ∷ p → p → p → p → p → p → () Source #

d_IsDistributiveLattice_814 ∷ p → p → p → p → p → p → () Source #

d_IsNearSemiring_876 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutOne_952 ∷ p → p → p → p → p → p → p → () Source #

d_IsCommutativeSemiringWithoutOne_1044 ∷ p → p → p → p → p → p → p → () Source #

d_IsSemiringWithoutAnnihilatingZero_1142 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsSemiring_1238 ∷ p → p → p → p → p → p → p → p → () Source #

d_setoid_1320T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsSemiring_1238T_Setoid_44 Source #

d_zero'691'_1332T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsSemiring_1238AgdaAnyAgdaAny Source #

d_zero'737'_1334T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsSemiring_1238AgdaAnyAgdaAny Source #

d_IsCommutativeSemiring_1344 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsCancellativeCommutativeSemiring_1462 ∷ p → p → p → p → p → p → p → p → () Source #

d_IsRing_1584 ∷ p → p → p → p → p → p → p → p → p → () Source #

d__'45'__1614T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'691'_1622T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'737'_1624T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_identity'691'_1628T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAny Source #

d_identity'737'_1630T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAny Source #

d_inverse'691'_1650T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAny Source #

d_inverse'737'_1652T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAny Source #

d_reflexive_1660T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAnyT__'8801'__12AgdaAny Source #

d_setoid_1662T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584T_Setoid_44 Source #

d_'8729''45'cong'691'_1678T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_'8729''45'cong'737'_1680T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_identity'691'_1684T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAny Source #

d_identity'737'_1686T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAny Source #

d_zero'737'_1692T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAny Source #

d_zero'691'_1694T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAny Source #

d_distrib'691'_1702T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_distrib'737'_1704T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsRing_1584AgdaAnyAgdaAnyAgdaAnyAgdaAny Source #

d_IsCommutativeRing_1720 ∷ p → p → p → p → p → p → p → p → p → () Source #

d__'45'__1742T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → AgdaAnyAgdaAnyT_IsCommutativeRing_1720AgdaAnyAgdaAnyAgdaAny Source #

d_identity'691'_1754T_Level_18T_Level_18 → () → (AgdaAnyAgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAny