| Safe Haskell | None |
|---|
MAlonzo.Code.Algebra.Construct.Subst.Equality
Documentation
d_cong'8321'_38 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_cong'8321'_38 :: T_Σ_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_cong'8322'_46 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_cong'8322'_46 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_assoc_56 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_assoc_56 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_comm_68 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_comm_68 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_idem_78 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #
du_idem_78 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #
d_sel_86 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #
du_sel_86 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #
d_identity_98 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 -> T_Σ_14 Source #
d_inverse_110 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 -> T_Σ_14 Source #
du_inverse_110 :: T_Σ_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 -> T_Σ_14 Source #
d_absorptive_120 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 Source #
du_absorptive_120 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 Source #
d_distrib'737'_138 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_distrib'737'_138 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_distrib'691'_152 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_distrib'691'_152 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_distrib_166 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 Source #
du_distrib_166 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 Source #
d_isMagma_174 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> T_IsMagma_98 Source #
du_isMagma_174 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsMagma_98 -> T_IsMagma_98 Source #
d_isSemigroup_206 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_206 -> T_IsSemigroup_206 Source #
du_isSemigroup_206 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_206 -> T_IsSemigroup_206 Source #
d_isBand_244 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_IsBand_242 Source #
du_isBand_244 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsBand_242 -> T_IsBand_242 Source #
d_isSelectiveMagma_286 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSelectiveMagma_170 -> T_IsSelectiveMagma_170 Source #
du_isSelectiveMagma_286 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSelectiveMagma_170 -> T_IsSelectiveMagma_170 Source #
d_isMonoid_324 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> T_IsMonoid_370 Source #
du_isMonoid_324 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsMonoid_370 -> T_IsMonoid_370 Source #
d_isCommutativeMonoid_376 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> T_IsCommutativeMonoid_420 Source #
du_isCommutativeMonoid_376 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeMonoid_420 -> T_IsCommutativeMonoid_420 Source #
d_isIdempotentCommutativeMonoid_432 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsIdempotentCommutativeMonoid_480 Source #
du_isIdempotentCommutativeMonoid_432 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsIdempotentCommutativeMonoid_480 -> T_IsIdempotentCommutativeMonoid_480 Source #
d_isGroup_498 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> T_IsGroup_652 Source #
du_isGroup_498 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsGroup_652 -> T_IsGroup_652 Source #
d_isAbelianGroup_572 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsAbelianGroup_740 Source #
du_isAbelianGroup_572 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> (AgdaAny -> AgdaAny) -> T_IsAbelianGroup_740 -> T_IsAbelianGroup_740 Source #
d_isNearSemiring_652 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> T_IsNearSemiring_826 Source #
du_isNearSemiring_652 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsNearSemiring_826 -> T_IsNearSemiring_826 Source #
d_isSemiringWithoutOne_728 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> T_IsSemiringWithoutOne_906 Source #
du_isSemiringWithoutOne_728 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsSemiringWithoutOne_906 -> T_IsSemiringWithoutOne_906 Source #
d_isCommutativeSemiringWithoutOne_786 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeSemiringWithoutOne_968 Source #
du_isCommutativeSemiringWithoutOne_786 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_IsCommutativeSemiringWithoutOne_968 -> T_IsCommutativeSemiringWithoutOne_968 Source #