Documentation

d_Digit_4 ∷ Integer → () Source #

d_Decimal_8 ∷ () Source #

d_Bit_10 ∷ () Source #

d_0b_12 ∷ T_Fin_10 Source #

d_1b_14 ∷ T_Fin_10 Source #

d_toNatDigits_20 ∷ Integer → AgdaAny → Integer → [Integer] Source #

du_toNatDigits_20 ∷ Integer → Integer → [Integer] Source #

d_aux_36 ∷ Integer → T_'8868'_6 → Integer → Integer → T_Acc_42 → [Integer] → [Integer] Source #

du_aux_36 ∷ Integer → Integer → [Integer] → [Integer] Source #

d_Expansion_62 ∷ Integer → () Source #

d_fromDigits_68 ∷ Integer → [T_Fin_10] → Integer Source #

d_toDigits_84 ∷ Integer → AgdaAny → Integer → T_Σ_14 Source #

du_toDigits_84 ∷ Integer → Integer → T_Σ_14 Source #

d_Pred_96 ∷ Integer → T_'8868'_6 → Integer → Integer → () Source #

d_cons_106 ∷ Integer → T_'8868'_6 → Integer → Integer → T_Fin_10 → T_Σ_14 → T_Σ_14 Source #

du_cons_106 ∷ T_Fin_10 → T_Σ_14 → T_Σ_14 Source #

d_lem'8242'_120 ∷ Integer → T_'8868'_6 → Integer → Integer → Integer → T__'8801'__12 Source #

d_lem_144 ∷ Integer → T_'8868'_6 → Integer → Integer → Integer → Integer → T__'8804''8242'__338 Source #

du_lem_144 ∷ Integer → Integer → Integer → T__'8804''8242'__338 Source #

d_helper_166 ∷ Integer → T_'8868'_6 → Integer → Integer → (Integer → T__'8804''8242'__338 → T_Σ_14) → T_Σ_14 Source #

du_helper_166 ∷ Integer → Integer → (Integer → T__'8804''8242'__338 → T_Σ_14) → T_Σ_14 Source #

d_digitChars_192 ∷ T_Vec_28 Source #

d_showDigit_198 ∷ Integer → AgdaAny → T_Fin_10 → T_Char_6 Source #

du_showDigit_198 ∷ T_Fin_10 → T_Char_6 Source #