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_206T_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_222T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48T_Any_34T_Any_34 Source #

d_tabulate'8314'_270T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → Integer → (T_Fin_10AgdaAny) → (T_Fin_10AgdaAny) → (T_Fin_10AgdaAny) → T_Pointwise_48 Source #

d_tabulate'8315'_286T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → Integer → (T_Fin_10AgdaAny) → (T_Fin_10AgdaAny) → T_Pointwise_48T_Fin_10AgdaAny Source #

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

d_map'8314'_394T_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'_416T_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'_446T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → [AgdaAny] → [AgdaAny] → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → AgdaAnyAgdaAnyAgdaAnyT_Pointwise_48AgdaAny Source #

d_filter'8314'_492T_Level_18 → () → T_Level_18T_Level_18 → () → T_Level_18T_Level_18 → (AgdaAnyAgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAnyT_Dec_20) → (AgdaAnyT_Dec_20) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → (AgdaAnyAgdaAnyAgdaAnyAgdaAnyAgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48T_Pointwise_48 Source #

d_lookup'8314'_572T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAnyAgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48T_Fin_10AgdaAny Source #