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

du_just'45'equivalence_54 ∷ T_Equivalence_16 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_170 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawIApplicative_38 → Maybe AgdaAny → T_All_18 → AgdaAny Source #

du_sequenceA_170 ∷ T_RawIApplicative_38 → T_All_18 → AgdaAny Source #

d_mapA_178 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawIApplicative_38 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 → AgdaAny Source #

du_mapA_178 ∷ T_RawIApplicative_38 → (AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 → AgdaAny Source #

d_forA_188 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawIApplicative_38 → T_Level_18 → (AgdaAny → ()) → Maybe AgdaAny → T_All_18 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

du_forA_188 ∷ T_RawIApplicative_38 → Maybe AgdaAny → T_All_18 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

d_App_210 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawIMonad_32 → T_RawIApplicative_38 Source #

du_App_210 ∷ T_RawIMonad_32 → T_RawIApplicative_38 Source #

d_sequenceM_212 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawIMonad_32 → Maybe AgdaAny → T_All_18 → AgdaAny Source #

du_sequenceM_212 ∷ T_RawIMonad_32 → T_All_18 → AgdaAny Source #

d_mapM_218 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawIMonad_32 → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 → AgdaAny Source #

du_mapM_218 ∷ T_RawIMonad_32 → (AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → T_All_18 → AgdaAny Source #

d_forM_226 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (() → ()) → T_RawIMonad_32 → T_Level_18 → (AgdaAny → ()) → Maybe AgdaAny → T_All_18 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

du_forM_226 ∷ T_RawIMonad_32 → Maybe AgdaAny → T_All_18 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny Source #

d_dec_240 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → T_Dec_32) → Maybe AgdaAny → T_Dec_32 Source #

du_dec_240 ∷ (AgdaAny → T_Dec_32) → Maybe AgdaAny → T_Dec_32 Source #

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

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

d_irrelevant_256 ∷ 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_266 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Σ_14 Source #

du_satisfiable_266 ∷ T_Σ_14 Source #