| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid
Documentation
d_AllPairs_20 ∷ p → p → p → p → () Source #
d__'8779'__76 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → () Source #
d_refl_84 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → T_Pointwise_48 Source #
du_refl_84 ∷ T_Setoid_46 → [AgdaAny] → T_Pointwise_48 Source #
d_reflexive_86 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Pointwise_48 Source #
du_reflexive_86 ∷ T_Setoid_46 → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Pointwise_48 Source #
d_sym_88 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_sym_88 ∷ T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_trans_90 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_trans_90 ∷ T_Setoid_46 → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_Unique'45'resp'45''8779'_92 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #
du_Unique'45'resp'45''8779'_92 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #
d_'8779''45'length_98 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T__'8801'__12 Source #
d__'8779''8242'__114 ∷ T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → () Source #
d_map'8314'_122 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_map'8314'_122 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_foldr'8314'_150 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_48 → AgdaAny Source #
du_foldr'8314'_150 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_48 → AgdaAny Source #
d_'43''43''8314'_158 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_'43''43''8314'_158 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_'43''43''8314''737'_162 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_'43''43''8314''691'_168 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_'43''43''8314''691'_168 ∷ T_Setoid_46 → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_'43''43''45'cancel'737'_178 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_'43''43''45'cancel'691'_188 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_concat'8314'_190 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [[AgdaAny]] → [[AgdaAny]] → T_Pointwise_48 → T_Pointwise_48 Source #
du_concat'8314'_190 ∷ [[AgdaAny]] → [[AgdaAny]] → T_Pointwise_48 → T_Pointwise_48 Source #
d_tabulate'8314'_204 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → T_Pointwise_48 Source #
du_tabulate'8314'_204 ∷ Integer → (T_Fin_10 → AgdaAny) → T_Pointwise_48 Source #
d_tabulate'8315'_208 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → T_Pointwise_48 → T_Fin_10 → AgdaAny Source #
d_filter'8314'_222 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_filter'8314'_222 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_'691''43''43''8314'_226 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_'691''43''43''8314'_226 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_reverse'8314'_228 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_reverse'8314'_228 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #