plutus-metatheory-1.70.0.0: Command line tool for running plutus core programs
Safe HaskellSafe-Inferred
LanguageHaskell2010

MAlonzo.Code.Data.List.Relation.Unary.Any.Properties

Documentation

d__'62''62''61'__38 ∷ T_Level_18 → () → () → [AgdaAny] → (AgdaAny → [AgdaAny]) → [AgdaAny] Source #

d__'8855'__40 ∷ T_Level_18 → () → () → [AgdaAny] → [AgdaAny] → [T_Σ_14] Source #

du__'8855'__40 ∷ () → () → [AgdaAny] → [AgdaAny] → [T_Σ_14] Source #

d__'8859'__42 ∷ T_Level_18 → () → () → [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du__'8859'__42 ∷ () → () → [AgdaAny → AgdaAny] → [AgdaAny] → [AgdaAny] Source #

du_pure_50 ∷ () → AgdaAny → [AgdaAny] Source #

d_lift'45'resp_102 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Any_34 → T_Any_34 Source #

d_Any'45'cong_140 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Kind_6 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny Source #

d_map'45'cong_172 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → T_Any_34 → T__'8801'__12 Source #

d_map'45'id_198 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12) → T_Any_34 → T__'8801'__12 Source #

d_map'45''8728'_218 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Any_34 → T__'8801'__12 Source #

d_swap_264 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_swap'45'there_274 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → AgdaAny → T_Any_34 → T__'8801'__12 Source #

d_swap'45'invol_296 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Any_34 → T__'8801'__12 Source #

d_swap'8596'_320 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #

d_from_328 ∷ T_Level_18 → () → [AgdaAny] → T_Level_18 → () → [AgdaAny] → T_Level_18 → () → T_Any_34 → AgdaAny Source #

d_'8846''8596'_424 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → T_Inverse_2122 Source #

d_from'8728'to_436 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T__'8846'__30 → T__'8801'__12 Source #

d_to'8728'from_458 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T__'8801'__12 Source #

d_Any'45''215''8314'_482 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Σ_14 → T_Any_34 Source #

d_Any'45''215''8315'_496 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_'215''8596'_522 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #

d_from'8728'to_538 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Σ_14 → T__'8801'__12 Source #

d_to'8728'from_630 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Any_34 → T__'8801'__12 Source #

d_Any'45'Σ'8314''691'_690 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → T_Σ_14 → T_Any_34 Source #

d_Any'45'Σ'8315''691'_704 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_map'8314'_730 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_map'8315'_736 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_map'8596'_780 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Inverse_2122 Source #

d_gmap_782 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_mapMaybe'8314'_798 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → Maybe AgdaAny) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_concat'8314'_1086 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #

d_concat'8315'_1096 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [[AgdaAny]] → T_Any_34 → T_Any_34 Source #

d_concatMap'8314'_1274 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_concatMap'8315'_1276 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → [AgdaAny]) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_cartesianProductWith'8314'_1294 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Any_34 → T_Any_34 → T_Any_34 Source #

d_cartesianProductWith'8315'_1316 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → T_Σ_14) → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_cartesianProduct'8314'_1362 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #

d_cartesianProduct'8315'_1368 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_filter'8314'_1518 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T__'8846'__30 Source #

d_filter'8315'_1554 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_derun'8314''45'aux_1606 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Any_34 Source #

d_derun'8314'_1650 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Any_34 → T_Any_34 Source #

d_deduplicate'8314'_1696 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Any_34 → T_Any_34 Source #

d_derun'8315''45'aux_1740 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_derun'8315'_1780 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_deduplicate'8315'_1788 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_mapWith'8712''8314'_1818 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_Σ_14 → T_Any_34 Source #

d_mapWith'8712''8315'_1840 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_Any_34 → T_Σ_14 Source #

d_from'8728'to_1886 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_Σ_14 → T__'8801'__12 Source #

d_to'8728'from_1910 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_Level_18 → () → [AgdaAny] → (AgdaAny → T_Any_34 → AgdaAny) → T_Any_34 → T__'8801'__12 Source #

d_'62''62''61''8596'_2080 ∷ T_Level_18 → T_Level_18 → () → () → (AgdaAny → ()) → (AgdaAny → [AgdaAny]) → [AgdaAny] → T_Inverse_2122 Source #

d_'8859''8596'_2096 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → ()) → [AgdaAny → AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #

d_'8859''8314''8242'_2132 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → [AgdaAny → AgdaAny] → [AgdaAny] → T_Any_34 → T_Any_34 → T_Any_34 Source #

d_'8855''8596'_2152 ∷ T_Level_18 → () → () → T_Level_18 → (T_Σ_14 → ()) → [AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #

d_'8855''8596''8242'_2186 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Inverse_2122 Source #