| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties
Documentation
d_reflexive_28 ∷ 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_reflexive_28 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_refl_30 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → [AgdaAny] → T_Pointwise_48 Source #
du_refl_30 ∷ (AgdaAny → AgdaAny) → [AgdaAny] → T_Pointwise_48 Source #
d_symmetric_40 ∷ 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_symmetric_40 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 Source #
d_transitive_50 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_transitive_50 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_antisymmetric_64 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_antisymmetric_64 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_resp'691'_78 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_resp'691'_78 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_resp'737'_92 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
du_resp'737'_92 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T_Pointwise_48 Source #
d_respects'8322'_106 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_decidable_112 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Dec_20 Source #
d_irrelevant_132 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Pointwise_48 → T__'8801'__12 Source #
d_Pointwise'45'length_150 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T__'8801'__12 Source #
d_lookup'45'cast_164 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T__'8801'__12 → T_Fin_10 → AgdaAny Source #
du_lookup'45'cast_164 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Fin_10 → AgdaAny Source #