| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
Documentation
d_Pointwise_48 ∷ p → p → p → p → p → p → p → p → () Source #
data T_Pointwise_48 Source #
Constructors
| C_'91''93'_56 | |
| C__'8759'__62 AgdaAny T_Pointwise_48 |
d_head_64 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → [AgdaAny] → T_Pointwise_48 → AgdaAny Source #
d_tail_70 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_uncons_76 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → [AgdaAny] → AgdaAny → [AgdaAny] → T_Pointwise_48 → T_Σ_14 Source #
d_rec_102 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → ([AgdaAny] → [AgdaAny] → T_Pointwise_48 → ()) → (AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → AgdaAny Source #
du_rec_102 ∷ (AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → AgdaAny Source #
d_map_120 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_map_120 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_unzip_130 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Σ_14 Source #
du_unzip_130 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Σ_14 Source #