| Safe Haskell | None |
|---|
MAlonzo.Code.Algebra.Definitions.RawSemiring
Documentation
d__'8777'__20 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> AgdaAny -> AgdaAny -> () Source #
d__'215'__40 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> Integer -> AgdaAny -> AgdaAny Source #
du__'215'__40 :: T_RawSemiring_1672 -> Integer -> AgdaAny -> AgdaAny Source #
d__'215''8242'__42 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> Integer -> AgdaAny -> AgdaAny Source #
du__'215''8242'__42 :: T_RawSemiring_1672 -> Integer -> AgdaAny -> AgdaAny Source #
d_sum_44 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> Integer -> (T_Fin_6 -> AgdaAny) -> AgdaAny Source #
d__'8739'__52 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> AgdaAny -> AgdaAny -> () Source #
d__'8740'__60 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> AgdaAny -> AgdaAny -> () Source #
d_sum_68 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> Integer -> (T_Fin_6 -> AgdaAny) -> AgdaAny Source #
d__'94'__70 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> AgdaAny -> Integer -> AgdaAny Source #
du__'94'__70 :: T_RawSemiring_1672 -> AgdaAny -> Integer -> AgdaAny Source #
d__'94''8242'__76 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> AgdaAny -> Integer -> AgdaAny Source #
du__'94''8242'__76 :: T_RawSemiring_1672 -> AgdaAny -> Integer -> AgdaAny Source #
d__'94''91'_'93''42'__82 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> AgdaAny -> Integer -> AgdaAny -> AgdaAny Source #
du__'94''91'_'93''42'__82 :: T_RawSemiring_1672 -> AgdaAny -> Integer -> AgdaAny -> AgdaAny Source #
d__'94''7511'__94 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> AgdaAny -> Integer -> AgdaAny Source #
du__'94''7511'__94 :: T_RawSemiring_1672 -> AgdaAny -> Integer -> AgdaAny Source #
d_Coprime_100 :: T_Level_14 -> T_Level_14 -> T_RawSemiring_1672 -> AgdaAny -> AgdaAny -> () Source #
d_Irreducible_110 :: p1 -> p2 -> p3 -> p4 -> () Source #
newtype T_Irreducible_110 Source #
Constructors
| C_mkIrred_130 (AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30) |
d_p'8740'1_122 :: T_Irreducible_110 -> T_Σ_14 -> T_'8869'_4 Source #
d_split'45''8739'1_128 :: T_Irreducible_110 -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #
d_Prime_134 :: p1 -> p2 -> p3 -> p4 -> () Source #
newtype T_Prime_134 Source #
Constructors
| C_mkPrime_158 (AgdaAny -> AgdaAny -> T_Σ_14 -> T__'8846'__30) |
d_p'8777'0_148 :: T_Prime_134 -> AgdaAny -> T_'8869'_4 Source #
d_p'8740'1_150 :: T_Prime_134 -> T_Σ_14 -> T_'8869'_4 Source #
d_split'45''8739'_156 :: T_Prime_134 -> AgdaAny -> AgdaAny -> T_Σ_14 -> T__'8846'__30 Source #