Documentation

d_Any_18 ∷ p → p → p → p → p → () Source #

newtype T_Any_18 Source #

d_drop'45'just_46 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → AgdaAny → T_Any_18 → AgdaAny Source #

du_drop'45'just_46 ∷ T_Any_18 → AgdaAny Source #

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

du_just'45'equivalence_52 ∷ T_Equivalence_1714 Source #

d_map_58 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → T_Any_18 → T_Any_18 Source #

du_map_58 ∷ (AgdaAny → AgdaAny → AgdaAny) → Maybe AgdaAny → T_Any_18 → T_Any_18 Source #

d_satisfied_66 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → Maybe AgdaAny → T_Any_18 → T_Σ_14 Source #

du_satisfied_66 ∷ Maybe AgdaAny → T_Any_18 → T_Σ_14 Source #

d_zipWith_90 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T_Σ_14 → AgdaAny) → Maybe AgdaAny → T_Σ_14 → T_Any_18 Source #

du_zipWith_90 ∷ (AgdaAny → T_Σ_14 → AgdaAny) → Maybe AgdaAny → T_Σ_14 → T_Any_18 Source #

d_unzipWith_98 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → T_Σ_14) → Maybe AgdaAny → T_Any_18 → T_Σ_14 Source #

du_unzipWith_98 ∷ (AgdaAny → AgdaAny → T_Σ_14) → Maybe AgdaAny → T_Any_18 → T_Σ_14 Source #

d_zip_120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → Maybe AgdaAny → T_Σ_14 → T_Any_18 Source #

du_zip_120 ∷ Maybe AgdaAny → T_Σ_14 → T_Any_18 Source #

d_unzip_122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → Maybe AgdaAny → T_Any_18 → T_Σ_14 Source #

du_unzip_122 ∷ Maybe AgdaAny → T_Any_18 → T_Σ_14 Source #

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

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

d_irrelevant_144 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → T__'8801'__12) → Maybe AgdaAny → T_Any_18 → T_Any_18 → T__'8801'__12 Source #

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

du_satisfiable_152 ∷ T_Σ_14 → T_Σ_14 Source #