| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Membership.Propositional.Properties
Documentation
d__'62''62''61'__30 ∷ T_Level_18 → () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny] → (AgdaAny → [AgdaAny]) → [AgdaAny] Source #
du__'62''62''61'__30 ∷ () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny] → (AgdaAny → [AgdaAny]) → [AgdaAny] Source #
d__'8855'__32 ∷ T_Level_18 → () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny] → [AgdaAny] → [T_Σ_14] Source #
du__'8855'__32 ∷ () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny] → [AgdaAny] → [T_Σ_14] Source #
d__'8859'__34 ∷ T_Level_18 → () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #
du__'8859'__34 ∷ () → () → T_'8868'_6 → T_'8868'_6 → T_'8868'_6 → [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #
d_'8712''45'resp'45''8779'_64 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #
du_'8712''45'resp'45''8779'_64 ∷ AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #
d_'8713''45'resp'45''8779'_70 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → (T_Any_34 → T_'8869'_4) → T_Any_34 → T_'8869'_4 Source #
d_mapWith'8712''45'cong_84 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → (AgdaAny → T_Any_34 → AgdaAny) → (AgdaAny → T_Any_34 → T__'8801'__12) → T__'8801'__12 Source #
d_mapWith'8712''8791'map_110 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_'8712''45'map'8314'_130 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45'map'8315'_138 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d_map'45''8712''8596'_146 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Inverse_58 Source #
d_'8712''45''43''43''8314''737'_172 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45''43''43''8314''691'_178 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45''43''43''8315'_184 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T__'8846'__30 Source #
d_'8712''45'insert_190 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 Source #
d_'8712''45''8707''43''43'_200 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d_'8712''45'concat'8314'_228 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #
d_'8712''45'concat'8315'_234 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #
d_'8712''45'concat'8314''8242'_240 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [[AgdaAny]] → T_Any_34 → T_Any_34 → T_Any_34 Source #
du_'8712''45'concat'8314''8242'_240 ∷ AgdaAny → [AgdaAny] → [[AgdaAny]] → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45'concat'8315''8242'_250 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Σ_14 Source #
d_concat'45''8712''8596'_274 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Inverse_58 Source #
d_'8712''45'cartesianProductWith'8314'_308 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → T_Any_34 Source #
du_'8712''45'cartesianProductWith'8314'_308 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45'cartesianProductWith'8315'_320 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → T_Any_34 → T_Σ_14 Source #
du_'8712''45'cartesianProductWith'8315'_320 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → T_Any_34 → T_Σ_14 Source #
d_'8712''45'cartesianProduct'8314'_330 ∷ T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #
du_'8712''45'cartesianProduct'8314'_330 ∷ AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45'cartesianProduct'8315'_342 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Σ_14 → T_Any_34 → T_Σ_14 Source #
d_'8712''45'applyUpTo'8314'_380 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → Integer → T__'8804'__18 → T_Any_34 Source #
du_'8712''45'applyUpTo'8314'_380 ∷ (Integer → AgdaAny) → Integer → T__'8804'__18 → T_Any_34 Source #
d_'8712''45'applyUpTo'8315'_388 ∷ T_Level_18 → () → (Integer → AgdaAny) → AgdaAny → Integer → T_Any_34 → T_Σ_14 Source #
d_'8712''45'applyDownFrom'8314'_424 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → Integer → T__'8804'__18 → T_Any_34 Source #
du_'8712''45'applyDownFrom'8314'_424 ∷ (Integer → AgdaAny) → Integer → Integer → T__'8804'__18 → T_Any_34 Source #
d_'8712''45'applyDownFrom'8315'_432 ∷ T_Level_18 → () → (Integer → AgdaAny) → AgdaAny → Integer → T_Any_34 → T_Σ_14 Source #
d_'8712''45'tabulate'8314'_470 ∷ T_Level_18 → () → Integer → (T_Fin_6 → AgdaAny) → T_Fin_6 → T_Any_34 Source #
d_'8712''45'tabulate'8315'_476 ∷ T_Level_18 → () → Integer → (T_Fin_6 → AgdaAny) → AgdaAny → T_Any_34 → T_Σ_14 Source #
d_'8712''45'filter'8314'_494 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → AgdaAny → [AgdaAny] → T_Any_34 → AgdaAny → T_Any_34 Source #
du_'8712''45'filter'8314'_494 ∷ (AgdaAny → T_Dec_32) → [AgdaAny] → T_Any_34 → AgdaAny → T_Any_34 Source #
d_'8712''45'filter'8315'_500 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
du_'8712''45'filter'8315'_500 ∷ (AgdaAny → T_Dec_32) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d_'8712''45'derun'8315'_518 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'derun'8315'_518 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45'deduplicate'8315'_528 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'deduplicate'8315'_528 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45'derun'8314'_546 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'derun'8314'_546 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
d_'8712''45'deduplicate'8314'_554 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'deduplicate'8314'_554 ∷ (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
d_'62''62''61''45''8712''8596'_570 ∷ T_Level_18 → () → () → [AgdaAny] → (AgdaAny → [AgdaAny]) → AgdaAny → T_Inverse_58 Source #
du_'62''62''61''45''8712''8596'_570 ∷ [AgdaAny] → (AgdaAny → [AgdaAny]) → T_Inverse_58 Source #
d_'8859''45''8712''8596'_596 ∷ T_Level_18 → () → () → [AgdaAny → AgdaAny] → [AgdaAny] → AgdaAny → T_Inverse_58 Source #
du_'8859''45''8712''8596'_596 ∷ [AgdaAny → AgdaAny] → [AgdaAny] → T_Inverse_58 Source #
d_'8855''45''8712''8596'_628 ∷ T_Level_18 → () → () → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Inverse_58 Source #
d_'8712''45'length_650 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Any_34 → T__'8804'__18 Source #
d_'8712''45'lookup_656 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_6 → T_Any_34 Source #
d_foldr'45'selective_674 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
du_foldr'45'selective_674 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
d_'91''93''8712'inits_688 ∷ T_Level_18 → () → [AgdaAny] → T_Any_34 Source #
d_finite_700 ∷ T_Level_18 → () → T_Injection_88 → [AgdaAny] → (Integer → T_Any_34) → T_'8869'_4 Source #
d_f_728 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → AgdaAny Source #
d_not'45'x_734 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → (T__'8801'__12 → T_'8869'_4) → T_Any_34 Source #
d_helper_758 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → T_Dec_32 → T_'8869'_4 Source #
d_f'8242'_772 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → AgdaAny Source #
du_f'8242'_772 ∷ T_Injection_88 → Integer → Integer → AgdaAny Source #
d_'8712''45'if'45'not'45'i_786 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → (T__'8801'__12 → T_'8869'_4) → T_Any_34 Source #
d_lemma_794 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → Integer → T__'8804'__18 → (T__'8804'__18 → T_'8869'_4) → T__'8801'__12 → T_'8869'_4 Source #
d_f'8242''11388''8712'xs_802 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → T_Any_34 Source #
d_f'8242''45'injective'8242'_818 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #
d_f'8242''45'inj_870 ∷ T_Level_18 → () → T_Injection_88 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → T_Injection_88 Source #
d_there'45'injective'45''8802''8712'_884 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → (T__'8801'__12 → T__'8801'__12 → T_'8869'_4) → T__'8801'__12 → T__'8801'__12 → T_'8869'_4 Source #
d_boolFilter'45''8712'_896 ∷ T_Level_18 → () → (AgdaAny → Bool) → [AgdaAny] → AgdaAny → T_Any_34 → T__'8801'__12 → T_Any_34 Source #
d_filter'45''8712'_944 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → AgdaAny → [AgdaAny] → T_Any_34 → AgdaAny → T_Any_34 Source #