| Safe Haskell | None |
|---|
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.Properties
Documentation
d_'61''91''93''8658'_44 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 Source #
du_'61''91''93''8658'_44 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 Source #
d__'126''7506'__62 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () Source #
d_fromSum_68 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8846'__30 -> T_ReflClosure_30 Source #
d_toSum_76 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T__'8846'__30 Source #
d_'8846''8660'Refl_84 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T_Equivalence_928 Source #
d_sym_86 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 Source #
du_sym_86 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 Source #
d_trans_94 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> T_ReflClosure_30 Source #
du_trans_94 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> T_ReflClosure_30 Source #
d_antisym_114 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny Source #
du_antisym_114 :: (AgdaAny -> AgdaAny) -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny Source #
d_total_140 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #
du_total_140 :: (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #
d_dec_174 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32 Source #
du_dec_174 :: (AgdaAny -> AgdaAny -> T_Dec_32) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32 Source #
d_decidable_184 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Dec_32 Source #
d_resp'737'_226 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny Source #
du_resp'737'_226 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny Source #
d_resp'691'_234 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny Source #
du_resp'691'_234 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny Source #
d_resp_250 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny Source #
du_resp_250 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny Source #
d_resp'8322'_270 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 Source #
du_resp'8322'_270 :: T_Σ_14 -> T_Σ_14 Source #
d__'126''7506'__282 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () Source #
d_isPreorder_284 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreorder_70 Source #
du_isPreorder_284 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsPreorder_70 Source #
d_isPartialOrder_290 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162 Source #
d_isDecPartialOrder_326 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecStrictPartialOrder_312 -> T_IsDecPartialOrder_206 Source #
d_isTotalOrder_374 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> T_IsTotalOrder_380 Source #
d_isDecTotalOrder_426 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> T_IsDecTotalOrder_430 Source #