| 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 #
du_reflexive_28 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 #
d_refl_30 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Pointwise_48 #
du_refl_30 :: (AgdaAny -> AgdaAny) -> [AgdaAny] -> T_Pointwise_48 #
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 #
du_symmetric_40 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 #
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 #
du_transitive_50 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 #
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 #
du_antisymmetric_64 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 #
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 #
du_resp'691'_78 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 #
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 #
du_resp'737'_92 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 #
d_respects'8322'_106 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 #
du_respects'8322'_106 :: T_Σ_14 -> T_Σ_14 #
d_decidable_112 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> [AgdaAny] -> [AgdaAny] -> T_Dec_20 #
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 #