Documentation

d_All_18 ∷ p → p → p → p → p → () Source #

data T_All_18 Source #

d_drop'45'just_48 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → T_All_18 → AgdaAny Source #

du_drop'45'just_48 ∷ T_All_18 → AgdaAny Source #

d_just'45'equivalence_54 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → T_Equivalence_1714 Source #

du_just'45'equivalence_54 ∷ T_Equivalence_1714 Source #

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 Source #

du_map_60 ∷ (AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 → T_All_18 Source #

d_fromAny_68 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → Maybe AgdaAny → T_Any_18 → T_All_18 Source #

du_fromAny_68 ∷ T_Any_18 → T_All_18 Source #

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 Source #

du_zipWith_92 ∷ (AgdaAny → T_Σ_14 → AgdaAny) → Maybe AgdaAny → T_Σ_14 → T_All_18 Source #

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 Source #

du_unzipWith_102 ∷ (AgdaAny → AgdaAny → T_Σ_14) → Maybe AgdaAny → T_All_18 → T_Σ_14 Source #

d_zip_126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → Maybe AgdaAny → T_Σ_14 → T_All_18 Source #

du_zip_126 ∷ Maybe AgdaAny → T_Σ_14 → T_All_18 Source #

d_unzip_128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → Maybe AgdaAny → T_All_18 → T_Σ_14 Source #

du_unzip_128 ∷ Maybe AgdaAny → T_All_18 → T_Σ_14 Source #

d_sequenceA_182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawApplicative_20 → Maybe AgdaAny → T_All_18 → AgdaAny Source #

du_sequenceA_182 ∷ T_RawApplicative_20 → T_All_18 → AgdaAny Source #

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 Source #

du_mapA_190 ∷ T_RawApplicative_20 → (AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 → AgdaAny Source #

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 Source #

du_forA_200 ∷ T_RawApplicative_20 → Maybe AgdaAny → T_All_18 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

d_App_224 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawMonad_24 → T_RawApplicative_20 Source #

du_App_224 ∷ T_RawMonad_24 → T_RawApplicative_20 Source #

d_sequenceM_226 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawMonad_24 → Maybe AgdaAny → T_All_18 → AgdaAny Source #

du_sequenceM_226 ∷ T_RawMonad_24 → T_All_18 → AgdaAny Source #

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 Source #

du_mapM_232 ∷ T_RawMonad_24 → (AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 → AgdaAny Source #

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 Source #

du_forM_240 ∷ T_RawMonad_24 → Maybe AgdaAny → T_All_18 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

d_dec_254 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → T_Dec_20) → Maybe AgdaAny → T_Dec_20 Source #

du_dec_254 ∷ (AgdaAny → T_Dec_20) → Maybe AgdaAny → T_Dec_20 Source #

d_universal_262 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 Source #

du_universal_262 ∷ (AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 Source #

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 Source #

d_satisfiable_280 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 Source #

du_satisfiable_280 ∷ T_Σ_14 Source #