| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Membership.Setoid.Properties
Documentation
d__'8713'__42 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_'8713''91''93'_56 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → T_Any_34 → T_Irrelevant_20 Source #
d__'8777'__72 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → () Source #
d__'8779'__94 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → () Source #
d__'8712'__154 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8713'__156 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'resp'45''8776'_172 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'resp'45''8776'_172 ∷ T_Setoid_46 → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 Source #
d_'8713''45'resp'45''8776'_182 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → (T_Any_34 → T_Irrelevant_20) → T_Any_34 → T_Irrelevant_20 Source #
d_'8712''45'resp'45''8779'_194 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #
du_'8712''45'resp'45''8779'_194 ∷ T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #
d_'8713''45'resp'45''8779'_200 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → (T_Any_34 → T_Irrelevant_20) → T_Any_34 → T_Irrelevant_20 Source #
d_'8713''8658'All'91''8777''93'_214 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → (T_Any_34 → T_Irrelevant_20) → T_All_44 Source #
d_All'91''8777''93''8658''8713'_222 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → T_All_44 → T_Any_34 → T_Irrelevant_20 Source #
d_index'45'injective_234 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 → T__'8801'__12 → AgdaAny Source #
du_index'45'injective_234 ∷ T_Setoid_46 → AgdaAny → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 → AgdaAny Source #
d__'8777'__260 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → () Source #
d_AllPairs_284 ∷ p → p → p → p → () Source #
d__'8712'__300 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_'8713''215''8712''8658''8777'_322 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → AgdaAny → [AgdaAny] → T_All_44 → T_Any_34 → AgdaAny → T_Irrelevant_20 Source #
d_unique'8658'irrelevant_334 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → [AgdaAny] → T_AllPairs_20 → AgdaAny → T_Any_34 → T_Any_34 → T__'8801'__12 Source #
d__'8776'__384 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → AgdaAny → () Source #
d__'8779'__432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → () Source #
d__'8779'__442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → () Source #
d__'8712'__446 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_mapWith'8712'_458 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → [AgdaAny] Source #
du_mapWith'8712'_458 ∷ T_Setoid_46 → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → [AgdaAny] Source #
d_mapWith'8712''45'cong_480 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → (AgdaAny → T_Any_34 → AgdaAny) → (AgdaAny → T_Any_34 → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_Pointwise_48 Source #
du_mapWith'8712''45'cong_480 ∷ T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → (AgdaAny → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → AgdaAny) → T_Pointwise_48 Source #
d_mapWith'8712''8791'map_512 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → [AgdaAny] → T_Pointwise_48 Source #
du_mapWith'8712''8791'map_512 ∷ T_Setoid_46 → (AgdaAny → AgdaAny) → [AgdaAny] → T_Pointwise_48 Source #
d__'8712'__558 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_mapWith'8712'_570 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → [AgdaAny] Source #
du_mapWith'8712'_570 ∷ T_Setoid_46 → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → [AgdaAny] Source #
d_length'45'mapWith'8712'_582 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T__'8801'__12 Source #
d_mapWith'8712''45'id_594 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → T__'8801'__12 Source #
d_map'45'mapWith'8712'_618 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → T_Level_18 → () → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → (AgdaAny → AgdaAny) → T__'8801'__12 Source #
d__'8776'__652 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → AgdaAny → () Source #
d__'8712'__700 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8759''61'__704 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Level_18 → [AgdaAny] → (AgdaAny → ()) → T_Any_34 → AgdaAny → [AgdaAny] Source #
du__'8759''61'__704 ∷ T_Level_18 → [AgdaAny] → (AgdaAny → ()) → T_Any_34 → AgdaAny → [AgdaAny] Source #
d__'8712'__716 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8759''61'__720 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Level_18 → [AgdaAny] → (AgdaAny → ()) → T_Any_34 → AgdaAny → [AgdaAny] Source #
du__'8759''61'__720 ∷ T_Level_18 → [AgdaAny] → (AgdaAny → ()) → T_Any_34 → AgdaAny → [AgdaAny] Source #
d_'8712''45'map'8314'_736 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 Source #
du_'8712''45'map'8314'_736 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45'map'8315'_750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → (AgdaAny → AgdaAny) → T_Any_34 → T_Σ_14 Source #
d_map'45''8759''61'_766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → AgdaAny → T_Any_34 → T__'8801'__12 Source #
d__'8712'__790 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8779'__818 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → () Source #
d_'8712''45''43''43''8314''737'_832 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45''43''43''8314''691'_840 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45''43''43''8315'_848 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T__'8846'__30 Source #
d_'8712''45''43''43''8314''8728''43''43''8315'_858 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T__'8801'__12 Source #
d_'8712''45''43''43''8315''8728''43''43''8314'_868 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T__'8846'__30 → T__'8801'__12 Source #
d_'8712''45''43''43''8596'_876 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #
d_'8712''45''43''43''45'comm_884 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45''43''43''45'comm'8728''43''43''45'comm_894 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T__'8801'__12 Source #
d_'8712''45''43''43''8596''43''43'_902 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #
d_'8712''45'insert_912 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Any_34 Source #
d_'8712''45''8707''43''43'_926 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d__'8712'__956 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8712'__964 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [[AgdaAny]] → () Source #
d_'8712''45'concat'8314'_974 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #
d_'8712''45'concat'8315'_982 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #
d_'8712''45'concat'8314''8242'_990 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → [[AgdaAny]] → T_Any_34 → T_Any_34 → T_Any_34 Source #
du_'8712''45'concat'8314''8242'_990 ∷ T_Setoid_46 → AgdaAny → [AgdaAny] → [[AgdaAny]] → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45'concat'8315''8242'_1000 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [[AgdaAny]] → T_Any_34 → T_Σ_14 Source #
d__'8712'__1036 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → [AgdaAny]) → [AgdaAny] → AgdaAny → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'concatMap'8314'_1040 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → [AgdaAny]) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'concatMap'8314'_1040 ∷ (AgdaAny → [AgdaAny]) → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45'concatMap'8315'_1044 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → [AgdaAny]) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'concatMap'8315'_1044 ∷ (AgdaAny → [AgdaAny]) → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d__'8712'__1058 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_reverse'8314'_1064 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_reverse'8315'_1070 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d__'8776'__1096 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → AgdaAny → AgdaAny → () Source #
d__'8776'__1120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → AgdaAny → AgdaAny → () Source #
d__'8712'__1168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8712'__1184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8712'__1200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'cartesianProductWith'8314'_1224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → T_Any_34 Source #
du_'8712''45'cartesianProductWith'8314'_1224 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45'cartesianProductWith'8315'_1240 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → AgdaAny → T_Any_34 → T_Σ_14 Source #
du_'8712''45'cartesianProductWith'8315'_1240 ∷ T_Setoid_46 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d_Carrier_1318 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → () Source #
d__'8712'__1362 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8712'__1378 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8712'__1394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Σ_14 → [T_Σ_14] → () Source #
d_'8712''45'cartesianProduct'8314'_1416 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #
du_'8712''45'cartesianProduct'8314'_1416 ∷ [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45'cartesianProduct'8315'_1428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Σ_14 → T_Any_34 → T_Σ_14 Source #
d__'8712'__1452 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'applyUpTo'8314'_1460 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (Integer → AgdaAny) → Integer → Integer → T__'8804'__22 → T_Any_34 Source #
du_'8712''45'applyUpTo'8314'_1460 ∷ T_Setoid_46 → (Integer → AgdaAny) → Integer → T__'8804'__22 → T_Any_34 Source #
d_'8712''45'applyUpTo'8315'_1472 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (Integer → AgdaAny) → Integer → T_Any_34 → T_Σ_14 Source #
d_'8712''45'applyDownFrom'8314'_1480 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (Integer → AgdaAny) → Integer → Integer → T__'8804'__22 → T_Any_34 Source #
du_'8712''45'applyDownFrom'8314'_1480 ∷ T_Setoid_46 → (Integer → AgdaAny) → Integer → Integer → T__'8804'__22 → T_Any_34 Source #
d_'8712''45'applyDownFrom'8315'_1492 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (Integer → AgdaAny) → Integer → T_Any_34 → T_Σ_14 Source #
d__'8712'__1514 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'tabulate'8314'_1522 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → Integer → (T_Fin_10 → AgdaAny) → T_Fin_10 → T_Any_34 Source #
du_'8712''45'tabulate'8314'_1522 ∷ T_Setoid_46 → (T_Fin_10 → AgdaAny) → T_Fin_10 → T_Any_34 Source #
d_'8712''45'tabulate'8315'_1534 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → Integer → (T_Fin_10 → AgdaAny) → AgdaAny → T_Any_34 → T_Σ_14 Source #
d__'8712'__1562 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'filter'8314'_1568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → AgdaAny → T_Any_34 Source #
d_'8712''45'filter'8315'_1620 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
du_'8712''45'filter'8315'_1620 ∷ T_Setoid_46 → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d__'8776'__1702 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → () Source #
d__'8776'__1726 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → () Source #
d__'8712'__1750 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → AgdaAny → [AgdaAny] → () Source #
d__'8712'__1766 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'map'8728'filter'8315'_1782 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Any_34 → T_Σ_14 Source #
du_'8712''45'map'8728'filter'8315'_1782 ∷ T_Setoid_46 → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_Any_34 → T_Σ_14 Source #
d_'8712''45'map'8728'filter'8314'_1798 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Any_34 Source #
du_'8712''45'map'8728'filter'8314'_1798 ∷ T_Setoid_46 → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Any_34 Source #
d__'8776'__1828 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → () Source #
d__'8712'__1832 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'derun'8314'_1838 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'derun'8314'_1838 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
d_'8712''45'derun'8315'_1848 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'derun'8315'_1848 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_'8712''45'deduplicate'8314'_1858 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'deduplicate'8314'_1858 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
d_'8712''45'deduplicate'8315'_1868 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45'deduplicate'8315'_1868 ∷ (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_deduplicate'45''8712''8660'_1878 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Equivalence_1858 Source #
du_deduplicate'45''8712''8660'_1878 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → AgdaAny → T_Equivalence_1858 Source #
d__'8712'__1894 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'length_1900 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → T_Any_34 → T__'8804'__22 Source #
d__'8712'__1922 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_'8712''45'lookup_1928 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → T_Fin_10 → T_Any_34 Source #
d__'8776'__1954 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #
d__'8712'__1964 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → () Source #
d_foldr'45'selective_1970 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
du_foldr'45'selective_1970 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → [AgdaAny] → T__'8846'__30 Source #
d__'8712'__2072 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8759''61'__2076 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → T_Level_18 → [AgdaAny] → (AgdaAny → ()) → T_Any_34 → AgdaAny → [AgdaAny] Source #
du__'8759''61'__2076 ∷ T_Level_18 → [AgdaAny] → (AgdaAny → ()) → T_Any_34 → AgdaAny → [AgdaAny] Source #
d_'8712''45''8759''61''8314''45'updated_2094 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → AgdaAny → AgdaAny → T_Any_34 → T_Any_34 Source #
du_'8712''45''8759''61''8314''45'updated_2094 ∷ T_Setoid_46 → [AgdaAny] → AgdaAny → T_Any_34 → T_Any_34 Source #
d_'8712''45''8759''61''8314''45'untouched_2110 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Any_34 → (AgdaAny → T_Irrelevant_20) → T_Any_34 → T_Any_34 Source #
du_'8712''45''8759''61''8314''45'untouched_2110 ∷ [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #
d_'8712''45''8759''61''8315'_2146 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → T_Any_34 → (AgdaAny → T_Irrelevant_20) → T_Any_34 → T_Any_34 Source #
d__'8712'__2188 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d__'8713'__2190 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → [AgdaAny] → () Source #
d_Any'45''8712''45'swap_2210 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #
du_Any'45''8712''45'swap_2210 ∷ T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #
d_All'45''8713''45'swap_2220 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → [AgdaAny] → [AgdaAny] → T_All_44 → T_All_44 Source #
d_Pointwise_45555 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #
d_Pointwise_83715 ∷ p → p → p → p → p → p → p → p → p → p → p → () Source #