Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Documentation
d__DistributesOver__18 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'691'__20 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'737'__22 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Commutative_38 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Identity_50 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftIdentity_64 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftZero_68 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightIdentity_76 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightZero_80 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Zero_84 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_IsAbelianGroup_88 ∷ p → p → p → p → p → p → p → () Source #
d_IsCommutativeMonoid_100 ∷ p → p → p → p → p → p → () Source #
d_IsCommutativeSemiring_106 ∷ p → p → p → p → p → p → p → p → () Source #
d_IsMonoid_120 ∷ p → p → p → p → p → p → () Source #
d_IsRing_124 ∷ p → p → p → p → p → p → p → p → p → () Source #
d_IsSemigroup_128 ∷ p → p → p → p → p → () Source #
d_IsCommutativeMonoid'737'_1514 ∷ p → p → p → p → p → p → () Source #
d_identity'691'_1558 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → AgdaAny → AgdaAny Source #
du_identity'691'_1558 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → AgdaAny → AgdaAny Source #
d_identity_1560 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → T_Σ_14 Source #
du_identity_1560 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → T_Σ_14 Source #
d_isCommutativeMonoid_1562 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → T_IsCommutativeMonoid_406 Source #
du_isCommutativeMonoid_1562 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'737'_1514 → T_IsCommutativeMonoid_406 Source #
d_IsCommutativeMonoid'691'_1568 ∷ p → p → p → p → p → p → () Source #
d_identity'737'_1612 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → AgdaAny → AgdaAny Source #
du_identity'737'_1612 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → AgdaAny → AgdaAny Source #
d_identity_1614 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → T_Σ_14 Source #
du_identity_1614 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → T_Σ_14 Source #
d_isCommutativeMonoid_1616 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → T_IsCommutativeMonoid_406 Source #
du_isCommutativeMonoid_1616 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeMonoid'691'_1568 → T_IsCommutativeMonoid_406 Source #
d_IsCommutativeSemiring'737'_1626 ∷ p → p → p → p → p → p → p → p → () Source #
d_'43''45'isCommutativeMonoid_1644 ∷ T_IsCommutativeSemiring'737'_1626 → T_IsCommutativeMonoid_406 Source #
d_'42''45'isCommutativeMonoid_1646 ∷ T_IsCommutativeSemiring'737'_1626 → T_IsCommutativeMonoid_406 Source #
d_distrib'691'_1648 ∷ T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_distrib'737'_1736 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_distrib'737'_1736 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_distrib_1738 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_Σ_14 Source #
du_distrib_1738 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemiring'737'_1626 → T_Σ_14 Source #
d_zero'691'_1740 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny Source #
du_zero'691'_1740 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'737'_1626 → AgdaAny → AgdaAny Source #
d_zero_1742 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_Σ_14 Source #
du_zero_1742 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_Σ_14 Source #
d_isCommutativeSemiring_1744 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_IsCommutativeSemiring_1344 Source #
du_isCommutativeSemiring_1744 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'737'_1626 → T_IsCommutativeSemiring_1344 Source #
d_IsCommutativeSemiring'691'_1754 ∷ p → p → p → p → p → p → p → p → () Source #
d_'43''45'isCommutativeMonoid_1772 ∷ T_IsCommutativeSemiring'691'_1754 → T_IsCommutativeMonoid_406 Source #
d_'42''45'isCommutativeMonoid_1774 ∷ T_IsCommutativeSemiring'691'_1754 → T_IsCommutativeMonoid_406 Source #
d_distrib'737'_1776 ∷ T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_distrib'691'_1864 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_distrib'691'_1864 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_distrib_1866 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_Σ_14 Source #
du_distrib_1866 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeSemiring'691'_1754 → T_Σ_14 Source #
d_zero'737'_1868 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny Source #
du_zero'737'_1868 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'691'_1754 → AgdaAny → AgdaAny Source #
d_zero_1870 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_Σ_14 Source #
du_zero_1870 ∷ (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_Σ_14 Source #
d_isCommutativeSemiring_1872 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_IsCommutativeSemiring_1344 Source #
du_isCommutativeSemiring_1872 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_IsCommutativeSemiring'691'_1754 → T_IsCommutativeSemiring_1344 Source #
d_IsRingWithoutAnnihilatingZero_1884 ∷ p → p → p → p → p → p → p → p → p → () Source #
d_'43''45'isAbelianGroup_1902 ∷ T_IsRingWithoutAnnihilatingZero_1884 → T_IsAbelianGroup_662 Source #
d_zero'737'_2002 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → AgdaAny → AgdaAny Source #
du_zero'737'_2002 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → AgdaAny → AgdaAny Source #
d_zero'691'_2004 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → AgdaAny → AgdaAny Source #
du_zero'691'_2004 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → AgdaAny → AgdaAny Source #
d_zero_2006 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → T_Σ_14 Source #
du_zero_2006 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → T_Σ_14 Source #
d_isRing_2008 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → T_IsRing_1584 Source #
du_isRing_2008 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → T_IsRingWithoutAnnihilatingZero_1884 → T_IsRing_1584 Source #