plutus-metatheory-1.69.0.0: Command line tool for running plutus core programs

Safe Haskell	Safe-Inferred
Language	Haskell2010

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

Documentation

d_Any_34 ∷ p → p → p → p → p → () Source #

data T_Any_34 Source #

Constructors

C_here_46 AgdaAny
C_there_54 T_Any_34

d_head_56 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → AgdaAny → (T_Any_34 → T_Irrelevant_20) → T_Any_34 → AgdaAny Source #

du_head_56 ∷ T_Any_34 → AgdaAny Source #

d_tail_66 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → (AgdaAny → T_Irrelevant_20) → T_Any_34 → T_Any_34 Source #

du_tail_66 ∷ T_Any_34 → T_Any_34 Source #

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

du_map_76 ∷ (AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → T_Any_34 → T_Any_34 Source #

d_index_86 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Fin_10 Source #

du_index_86 ∷ [AgdaAny] → T_Any_34 → T_Fin_10 Source #

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

du_lookup_94 ∷ [AgdaAny] → T_Any_34 → AgdaAny Source #

d__'8759''61'__102 ∷ T_Level_18 → () → T_Level_18 → [AgdaAny] → (AgdaAny → ()) → T_Any_34 → AgdaAny → [AgdaAny] Source #

du__'8759''61'__102 ∷ [AgdaAny] → T_Any_34 → AgdaAny → [AgdaAny] Source #

d__'9472'__114 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → [AgdaAny] Source #

du__'9472'__114 ∷ [AgdaAny] → T_Any_34 → [AgdaAny] Source #

d_satisfied_120 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → [AgdaAny] → T_Any_34 → T_Σ_14 Source #

du_satisfied_120 ∷ [AgdaAny] → T_Any_34 → T_Σ_14 Source #

d_toSum_126 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → T_Any_34 → T__'8846'__30 Source #

du_toSum_126 ∷ T_Any_34 → T__'8846'__30 Source #

d_fromSum_132 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → [AgdaAny] → T__'8846'__30 → T_Any_34 Source #

du_fromSum_132 ∷ T__'8846'__30 → T_Any_34 Source #

d_any'63'_138 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Dec_20 Source #

du_any'63'_138 ∷ (AgdaAny → T_Dec_20) → [AgdaAny] → T_Dec_20 Source #

d_satisfiable_148 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #

du_satisfiable_148 ∷ T_Σ_14 → T_Σ_14 Source #

d_any_154 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → [AgdaAny] → T_Dec_20 Source #