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

MAlonzo.Code.Data.List.Relation.Binary.Pointwise

Documentation

d_All'45'resp'45'Pointwise_194T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48T_All_44T_All_44 Source #

d_Any'45'resp'45'Pointwise_210T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48T_Any_34T_Any_34 Source #

d_tabulate'8314'_258T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → Integer → (T_Fin_6AgdaAny) → (T_Fin_6AgdaAny) → (T_Fin_6AgdaAny) → T_Pointwise_48 Source #

d_tabulate'8315'_274T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → Integer → (T_Fin_6AgdaAny) → (T_Fin_6AgdaAny) → T_Pointwise_48T_Fin_6AgdaAny Source #

d_concat'8314'_350T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → [[AgdaAny]] → [[AgdaAny]] → T_Pointwise_48T_Pointwise_48 Source #

d_map'8314'_382T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → T_Pointwise_48T_Pointwise_48 Source #

d_map'8315'_404T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAnyAgdaAny) → (AgdaAnyAgdaAny) → T_Pointwise_48T_Pointwise_48 Source #

d_foldr'8314'_434T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyT_Pointwise_48AgdaAny Source #

d_filter'8314'_480T_Level_18 → () → T_Level_18T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyT_Dec_32) → (AgdaAnyT_Dec_32) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48T_Pointwise_48 Source #

d_lookup'8315'_548T_Level_18 → () → [AgdaAny] → T_Level_18 → () → [AgdaAny] → T_Level_18 → (AgdaAnyAgdaAny → ()) → T__'8801'__12 → (T_Fin_6T_Fin_6T__'8801'__12AgdaAny) → T_Pointwise_48 Source #

d_lookup'8314'_560T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48T_Fin_6AgdaAny Source #

d_Rel_586T_Level_18T_Level_18T_Level_18 → () → () → (AgdaAnyAgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #