| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Membership.Propositional.Properties
Documentation
d__'62''62''61'__36 ∷ T_Level_18 → () → () → [AgdaAny] → (AgdaAny → [AgdaAny]) → [AgdaAny] Source #
d__'8855'__38 ∷ T_Level_18 → () → () → [AgdaAny] → [AgdaAny] → [T_Σ_14] Source #
d__'8859'__40 ∷ T_Level_18 → () → () → [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #
d_'8712''45'resp'45''8779'_76 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #
du_'8712''45'resp'45''8779'_76 ∷ AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #
d_'8713''45'resp'45''8779'_82 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → (T_Any_34 → T_Irrelevant_20) → T_Any_34 → T_Irrelevant_20 Source #
d_mapWith'8712''45'cong_96 ∷ 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_122 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → [AgdaAny] → T__'8801'__12 Source #
d_mapWith'8712''45'id_134 ∷ T_Level_18 → () → [AgdaAny] → T__'8801'__12 Source #
d_map'45'mapWith'8712'_144 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d_'8712''45'map'8314'_160 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45'map'8315'_168 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d_map'45''8712''8596'_176 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Inverse_1960 Source #
d_'8712''45''43''43''8314''737'_202 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45''43''43''8314''691'_208 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45''43''43''8315'_214 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T__'8846'__30 Source #
d_'8712''45'insert_220 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 Source #
d_'8712''45''8707''43''43'_230 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d_'8712''45'concat'8314'_256 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #
d_'8712''45'concat'8315'_262 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #
d_'8712''45'concat'8314''8242'_268 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → [[AgdaAny]] → T_Any_34 → T_Any_34 → T_Any_34 Source #
du_'8712''45'concat'8314''8242'_268 ∷ AgdaAny → [AgdaAny] → [[AgdaAny]] → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45'concat'8315''8242'_278 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Σ_14 Source #
d_concat'45''8712''8596'_294 ∷ T_Level_18 → () → AgdaAny → [[AgdaAny]] → T_Inverse_1960 Source #
d_'8712''45'cartesianProductWith'8314'_328 ∷ 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'_328 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45'cartesianProductWith'8315'_340 ∷ 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'_340 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → T_Any_34 → T_Σ_14 Source #
d_'8712''45'cartesianProduct'8314'_350 ∷ 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'_350 ∷ AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45'cartesianProduct'8315'_362 ∷ T_Level_18 → () → T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Σ_14 → T_Any_34 → T_Σ_14 Source #
d_'8712''45'applyUpTo'8314'_390 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → Integer → T__'8804'__22 → T_Any_34 Source #
du_'8712''45'applyUpTo'8314'_390 ∷ (Integer → AgdaAny) → Integer → T__'8804'__22 → T_Any_34 Source #
d_'8712''45'applyUpTo'8315'_398 ∷ T_Level_18 → () → (Integer → AgdaAny) → AgdaAny → Integer → T_Any_34 → T_Σ_14 Source #
d_'8712''45'applyDownFrom'8314'_432 ∷ T_Level_18 → () → (Integer → AgdaAny) → Integer → Integer → T__'8804'__22 → T_Any_34 Source #
du_'8712''45'applyDownFrom'8314'_432 ∷ (Integer → AgdaAny) → Integer → Integer → T__'8804'__22 → T_Any_34 Source #
d_'8712''45'applyDownFrom'8315'_440 ∷ T_Level_18 → () → (Integer → AgdaAny) → AgdaAny → Integer → T_Any_34 → T_Σ_14 Source #
d_'8712''45'tabulate'8314'_476 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → T_Fin_10 → T_Any_34 Source #
d_'8712''45'tabulate'8315'_482 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → AgdaAny → T_Any_34 → T_Σ_14 Source #
d_'8712''45'filter'8314'_500 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → T_Any_34 → AgdaAny → T_Any_34 Source #
du_'8712''45'filter'8314'_500 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → AgdaAny → T_Any_34 Source #
d_'8712''45'filter'8315'_506 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
du_'8712''45'filter'8315'_506 ∷ (AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d_'8712''45'derun'8315'_524 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'derun'8315'_524 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45'deduplicate'8315'_534 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'deduplicate'8315'_534 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45'derun'8314'_552 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'derun'8314'_552 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
d_'8712''45'deduplicate'8314'_560 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'deduplicate'8314'_560 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
d_'62''62''61''45''8712''8596'_576 ∷ T_Level_18 → () → () → [AgdaAny] → (AgdaAny → [AgdaAny]) → AgdaAny → T_Inverse_1960 Source #
du_'62''62''61''45''8712''8596'_576 ∷ [AgdaAny] → (AgdaAny → [AgdaAny]) → T_Inverse_1960 Source #
d_'8859''45''8712''8596'_602 ∷ T_Level_18 → () → () → [AgdaAny → AgdaAny] → [AgdaAny] → AgdaAny → T_Inverse_1960 Source #
du_'8859''45''8712''8596'_602 ∷ [AgdaAny → AgdaAny] → [AgdaAny] → T_Inverse_1960 Source #
d_'8855''45''8712''8596'_634 ∷ T_Level_18 → () → () → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Inverse_1960 Source #
d_'8712''45'length_658 ∷ T_Level_18 → () → AgdaAny → [AgdaAny] → T_Any_34 → T__'8804'__22 Source #
d_'8712''45'lookup_664 ∷ T_Level_18 → () → [AgdaAny] → T_Fin_10 → T_Any_34 Source #
d_foldr'45'selective_682 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
du_foldr'45'selective_682 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
d_'91''93''8712'inits_696 ∷ T_Level_18 → () → [AgdaAny] → T_Any_34 Source #
d_finite_704 ∷ T_Level_18 → () → T_Injection_776 → [AgdaAny] → (Integer → T_Any_34) → T_Irrelevant_20 Source #
d_f_784 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → AgdaAny Source #
d_not'45'x_788 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → (T__'8801'__12 → T_Irrelevant_20) → T_Any_34 Source #
d_helper_812 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → T_Dec_20 → T_Irrelevant_20 Source #
d_f'8242'_826 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → AgdaAny Source #
d_'8712''45'if'45'not'45'i_840 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → (T__'8801'__12 → T_Irrelevant_20) → T_Any_34 Source #
d_lemma_848 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → Integer → T__'8804'__22 → (T__'8804'__22 → T_Irrelevant_20) → T__'8801'__12 → T_Irrelevant_20 Source #
d_f'8242''11388''8712'xs_856 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → T_Any_34 Source #
d_f'8242''45'injective'8242'_872 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → Integer → Integer → T__'8801'__12 → T__'8801'__12 Source #
d_f'8242''45'inj_924 ∷ T_Level_18 → () → T_Injection_776 → AgdaAny → [AgdaAny] → (Integer → T_Any_34) → Integer → T__'8801'__12 → T_Injection_776 Source #
d_there'45'injective'45''8802''8712'_938 ∷ T_Level_18 → () → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → (T__'8801'__12 → T__'8801'__12 → T_Irrelevant_20) → T__'8801'__12 → T__'8801'__12 → T_Irrelevant_20 Source #