| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Relation.Binary.Equality.Propositional
Documentation
d__'8779'__18 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → () Source #
d_'43''43''45'cancel'691'_20 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_'43''43''45'cancel'691'_20 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_'43''43''45'cancel'737'_22 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_'43''43''45'cancel'737'_22 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_'43''43''8314'_24 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_'43''43''8314'_24 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_Unique'45'resp'45''8779'_26 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #
du_Unique'45'resp'45''8779'_26 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #
d_concat'8314'_28 ∷ T_Level_18 → () → [[AgdaAny]] → [[AgdaAny]] → T_Pointwise_48 → T_Pointwise_48 Source #
du_concat'8314'_28 ∷ [[AgdaAny]] → [[AgdaAny]] → T_Pointwise_48 → T_Pointwise_48 Source #
d_filter'8314'_30 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_filter'8314'_30 ∷ T_Level_18 → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_foldr'8314'_32 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → T__'8801'__12 → T_Pointwise_48 → T__'8801'__12 Source #
d_map'8314'_34 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_map'8314'_34 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_reverse'8314'_36 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_reverse'8314'_36 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_tabulate'8314'_38 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → (T_Fin_10 → T__'8801'__12) → T_Pointwise_48 Source #
du_tabulate'8314'_38 ∷ Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → (T_Fin_10 → T__'8801'__12) → T_Pointwise_48 Source #
d_Pointwise_39 ∷ p → p → p → p → p → p → p → p → p → p → () Source #
d_tabulate'8315'_40 ∷ T_Level_18 → () → Integer → (T_Fin_10 → AgdaAny) → (T_Fin_10 → AgdaAny) → T_Pointwise_48 → T_Fin_10 → T__'8801'__12 Source #
d_'691''43''43''8314'_42 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_'691''43''43''8314'_42 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_'8779''45'length_46 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T__'8801'__12 Source #
d_'8779''45'refl_48 ∷ T_Level_18 → () → [AgdaAny] → T_Pointwise_48 Source #
d_'8779''45'reflexive_50 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Pointwise_48 Source #
d_'8779''45'setoid_52 ∷ T_Level_18 → () → T_Setoid_44 Source #
d_'8779''45'sym_54 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
du_'8779''45'sym_54 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_'8779''45'trans_56 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_'8779''45'trans_56 ∷ [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_All'45'resp'45'Pointwise_64 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #
du_All'45'resp'45'Pointwise_64 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_All_44 → T_All_44 Source #
d_AllPairs'45'resp'45'Pointwise_66 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #
du_AllPairs'45'resp'45'Pointwise_66 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_AllPairs_20 → T_AllPairs_20 Source #
d_Any'45'resp'45'Pointwise_68 ∷ T_Level_18 → () → 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 #
du_Any'45'resp'45'Pointwise_68 ∷ 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_'8779''8658''8801'_72 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T__'8801'__12 Source #
d_'8801''8658''8779'_78 ∷ T_Level_18 → () → [AgdaAny] → [AgdaAny] → T__'8801'__12 → T_Pointwise_48 Source #