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_recompute'45'irrelevant'45'id_68 ∷ T_Level_18 → () → T_Dec_20 → (AgdaAny → AgdaAny → T__'8801'__12) → AgdaAny → T__'8801'__12 Source #

d_T'63'_72 ∷ Bool → T_Dec_20 Source #

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

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

d_'8868''45'dec_82 ∷ T_Level_18 → T_Dec_20 Source #

du_'8868''45'dec_82 ∷ T_Dec_20 Source #

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

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

d_'8869''45'dec_94 ∷ T_Level_18 → T_Dec_20 Source #

du_'8869''45'dec_94 ∷ T_Dec_20 Source #

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

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

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

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

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

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

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

du_toSum_120 ∷ T_Dec_20 → T__'8846'__30 Source #

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

du_fromSum_126 ∷ T__'8846'__30 → T_Dec_20 Source #

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

du_isYes_132 ∷ T_Dec_20 → Bool Source #

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

du_isNo_134 ∷ T_Dec_20 → Bool Source #

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

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

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

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

du_toWitness_144 ∷ T_Dec_20 → AgdaAny Source #

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

du_fromWitness_150 ∷ T_Dec_20 → AgdaAny → AgdaAny Source #

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

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

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

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

du_from'45'yes_168 ∷ T_Dec_20 → AgdaAny Source #

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

du_from'45'no_174 ∷ T_Dec_20 → AgdaAny Source #

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

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

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

du_decidable'45'stable_198 ∷ T_Dec_20 → AgdaAny Source #

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

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

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

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

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

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

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