Documentation

d_All_18 :: p -> p -> p -> p -> p -> () #

data T_All_18 #

d_drop'45'just_48 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> AgdaAny -> T_All_18 -> AgdaAny #

du_drop'45'just_48 :: T_All_18 -> AgdaAny #

d_just'45'equivalence_54 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> AgdaAny -> T_Equivalence_1714 #

du_just'45'equivalence_54 :: T_Equivalence_1714 #

d_map_60 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T_All_18 -> T_All_18 #

du_map_60 :: (AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T_All_18 -> T_All_18 #

d_fromAny_68 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> Maybe AgdaAny -> T_Any_18 -> T_All_18 #

du_fromAny_68 :: T_Any_18 -> T_All_18 #

d_zipWith_92 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> T_Σ_14 -> AgdaAny) -> Maybe AgdaAny -> T_Σ_14 -> T_All_18 #

du_zipWith_92 :: (AgdaAny -> T_Σ_14 -> AgdaAny) -> Maybe AgdaAny -> T_Σ_14 -> T_All_18 #

d_unzipWith_102 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Σ_14) -> Maybe AgdaAny -> T_All_18 -> T_Σ_14 #

du_unzipWith_102 :: (AgdaAny -> AgdaAny -> T_Σ_14) -> Maybe AgdaAny -> T_All_18 -> T_Σ_14 #

d_zip_126 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> Maybe AgdaAny -> T_Σ_14 -> T_All_18 #

du_zip_126 :: Maybe AgdaAny -> T_Σ_14 -> T_All_18 #

d_unzip_128 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> Maybe AgdaAny -> T_All_18 -> T_Σ_14 #

du_unzip_128 :: Maybe AgdaAny -> T_All_18 -> T_Σ_14 #

d_sequenceA_182 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (() -> ()) -> T_RawApplicative_20 -> Maybe AgdaAny -> T_All_18 -> AgdaAny #

du_sequenceA_182 :: T_RawApplicative_20 -> T_All_18 -> AgdaAny #

d_mapA_190 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (() -> ()) -> T_RawApplicative_20 -> T_Level_18 -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T_All_18 -> AgdaAny #

du_mapA_190 :: T_RawApplicative_20 -> (AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T_All_18 -> AgdaAny #

d_forA_200 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (() -> ()) -> T_RawApplicative_20 -> T_Level_18 -> (AgdaAny -> ()) -> Maybe AgdaAny -> T_All_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny #

du_forA_200 :: T_RawApplicative_20 -> Maybe AgdaAny -> T_All_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny #

d_App_224 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (() -> ()) -> T_RawMonad_24 -> T_RawApplicative_20 #

du_App_224 :: T_RawMonad_24 -> T_RawApplicative_20 #

d_sequenceM_226 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (() -> ()) -> T_RawMonad_24 -> Maybe AgdaAny -> T_All_18 -> AgdaAny #

du_sequenceM_226 :: T_RawMonad_24 -> T_All_18 -> AgdaAny #

d_mapM_232 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (() -> ()) -> T_RawMonad_24 -> T_Level_18 -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T_All_18 -> AgdaAny #

du_mapM_232 :: T_RawMonad_24 -> (AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T_All_18 -> AgdaAny #

d_forM_240 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (() -> ()) -> T_RawMonad_24 -> T_Level_18 -> (AgdaAny -> ()) -> Maybe AgdaAny -> T_All_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny #

du_forM_240 :: T_RawMonad_24 -> Maybe AgdaAny -> T_All_18 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny #

d_dec_254 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> T_Dec_20) -> Maybe AgdaAny -> T_Dec_20 #

du_dec_254 :: (AgdaAny -> T_Dec_20) -> Maybe AgdaAny -> T_Dec_20 #

d_universal_262 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T_All_18 #

du_universal_262 :: (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T_All_18 #

d_irrelevant_270 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12) -> Maybe AgdaAny -> T_All_18 -> T_All_18 -> T__'8801'__12 #

d_satisfiable_280 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> ()) -> T_Σ_14 #

du_satisfiable_280 :: T_Σ_14 #