Documentation

d_decidable'45'stable_26 ∷ T_Level_18 → () → T_Dec_32 → ((AgdaAny → T_'8869'_4) → T_'8869'_4) → AgdaAny Source #

du_decidable'45'stable_26 ∷ T_Dec_32 → AgdaAny Source #

d_'172''45'drop'45'Dec_36 ∷ T_Level_18 → () → T_Dec_32 → T_Dec_32 Source #

du_'172''45'drop'45'Dec_36 ∷ T_Dec_32 → T_Dec_32 Source #

d_'172''172''45'Monad_42 ∷ T_Level_18 → T_RawIMonad_32 Source #

du_'172''172''45'Monad_42 ∷ T_RawIMonad_32 Source #

d_'172''172''45'push_56 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (((AgdaAny → AgdaAny) → T_'8869'_4) → T_'8869'_4) → AgdaAny → (AgdaAny → T_'8869'_4) → T_'8869'_4 Source #

d_excluded'45'middle_66 ∷ T_Level_18 → () → (T_Dec_32 → T_'8869'_4) → T_'8869'_4 Source #

d_call'47'cc_72 ∷ T_Level_18 → () → T_Level_18 → () → ((AgdaAny → AgdaAny) → (AgdaAny → T_'8869'_4) → T_'8869'_4) → (AgdaAny → T_'8869'_4) → T_'8869'_4 Source #

d_independence'45'of'45'premise_88 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → ()) → AgdaAny → (AgdaAny → T_Σ_14) → (T_Σ_14 → T_'8869'_4) → T_'8869'_4 Source #

d_helper_100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → ()) → AgdaAny → (AgdaAny → T_Σ_14) → T_Dec_32 → T_Σ_14 Source #

du_helper_100 ∷ AgdaAny → (AgdaAny → T_Σ_14) → T_Dec_32 → T_Σ_14 Source #

d_independence'45'of'45'premise'45''8846'_106 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T__'8846'__30) → (T__'8846'__30 → T_'8869'_4) → T_'8869'_4 Source #

d_helper_116 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T__'8846'__30) → T_Dec_32 → T__'8846'__30 Source #

du_helper_116 ∷ (AgdaAny → T__'8846'__30) → T_Dec_32 → T__'8846'__30 Source #

d_Excluded'45'Middle_152 ∷ T_Level_18 → () Source #

d_Double'45'Negation'45'Elimination_160 ∷ T_Level_18 → () Source #