Documentation

d_Dec_20 ∷ p → p → () Source #

data T_Dec_20 Source #

d_does_28 ∷ T_Dec_20 → Bool Source #

d_proof_30 ∷ T_Dec_20 → T_Reflects_16 Source #

d_From'45'yes_50 ∷ T_Level_18 → () → T_Dec_20 → () Source #

d_From'45'no_52 ∷ T_Level_18 → () → T_Dec_20 → () Source #

d_recompute_54 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → AgdaAny Source #

du_recompute_54 ∷ T_Dec_20 → AgdaAny → AgdaAny Source #

d_recompute'45'constant_62 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → AgdaAny → T__'8801'__12 Source #

d_T'63'_66 ∷ Bool → T_Dec_20 Source #

d_'172''63'_70 ∷ T_Level_18 → () → T_Dec_20 → T_Dec_20 Source #

du_'172''63'_70 ∷ T_Dec_20 → T_Dec_20 Source #

d__'215''45'dec__76 ∷ T_Level_18 → () → T_Level_18 → () → T_Dec_20 → T_Dec_20 → T_Dec_20 Source #

du__'215''45'dec__76 ∷ T_Dec_20 → T_Dec_20 → T_Dec_20 Source #

d__'8846''45'dec__86 ∷ T_Level_18 → () → T_Level_18 → () → T_Dec_20 → T_Dec_20 → T_Dec_20 Source #

du__'8846''45'dec__86 ∷ T_Dec_20 → T_Dec_20 → T_Dec_20 Source #

d__'8594''45'dec__96 ∷ T_Level_18 → () → T_Level_18 → () → T_Dec_20 → T_Dec_20 → T_Dec_20 Source #

du__'8594''45'dec__96 ∷ T_Dec_20 → T_Dec_20 → T_Dec_20 Source #

d_dec'8658'maybe_106 ∷ T_Level_18 → () → T_Dec_20 → Maybe AgdaAny Source #

du_dec'8658'maybe_106 ∷ T_Dec_20 → Maybe AgdaAny Source #

d_toSum_110 ∷ T_Level_18 → () → T_Dec_20 → T__'8846'__30 Source #

du_toSum_110 ∷ T_Dec_20 → T__'8846'__30 Source #

d_fromSum_116 ∷ T_Level_18 → () → T__'8846'__30 → T_Dec_20 Source #

du_fromSum_116 ∷ T__'8846'__30 → T_Dec_20 Source #

d_isYes_122 ∷ T_Level_18 → () → T_Dec_20 → Bool Source #

du_isYes_122 ∷ T_Dec_20 → Bool Source #

d_isNo_124 ∷ T_Level_18 → () → T_Dec_20 → Bool Source #

du_isNo_124 ∷ T_Dec_20 → Bool Source #

d_True_126 ∷ T_Level_18 → () → T_Dec_20 → () Source #

d_False_128 ∷ T_Level_18 → () → T_Dec_20 → () Source #

d_'8970'_'8971'_130 ∷ T_Level_18 → () → T_Dec_20 → Bool Source #

d_toWitness_134 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → AgdaAny Source #

du_toWitness_134 ∷ T_Dec_20 → AgdaAny Source #

d_fromWitness_140 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → AgdaAny Source #

du_fromWitness_140 ∷ T_Dec_20 → AgdaAny → AgdaAny Source #

d_toWitnessFalse_146 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny → AgdaAny → T_Irrelevant_20 Source #

d_fromWitnessFalse_152 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → T_Irrelevant_20) → AgdaAny Source #

du_fromWitnessFalse_152 ∷ T_Dec_20 → (AgdaAny → T_Irrelevant_20) → AgdaAny Source #

d_from'45'yes_158 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny Source #

du_from'45'yes_158 ∷ T_Dec_20 → AgdaAny Source #

d_from'45'no_164 ∷ T_Level_18 → () → T_Dec_20 → AgdaAny Source #

du_from'45'no_164 ∷ T_Dec_20 → AgdaAny Source #

d_map'8242'_168 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Dec_20 → T_Dec_20 Source #

du_map'8242'_168 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Dec_20 → T_Dec_20 Source #

d_decidable'45'stable_188 ∷ T_Level_18 → () → T_Dec_20 → ((AgdaAny → T_Irrelevant_20) → T_Irrelevant_20) → AgdaAny Source #

du_decidable'45'stable_188 ∷ T_Dec_20 → AgdaAny Source #

d_'172''45'drop'45'Dec_198 ∷ T_Level_18 → () → T_Dec_20 → T_Dec_20 Source #

du_'172''45'drop'45'Dec_198 ∷ T_Dec_20 → T_Dec_20 Source #

d_'172''172''45'excluded'45'middle_202 ∷ T_Level_18 → () → (T_Dec_20 → T_Irrelevant_20) → T_Irrelevant_20 Source #

d_excluded'45'middle_208 ∷ T_Level_18 → () → (T_Dec_20 → T_Irrelevant_20) → T_Irrelevant_20 Source #

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

d_fromDec_212 ∷ T_Level_18 → () → T_Dec_20 → T__'8846'__30 Source #

d_toDec_214 ∷ T_Level_18 → () → T__'8846'__30 → T_Dec_20 Source #