Documentation

d_Digit_4 ∷ Integer → () Source #

d_Decimal_8 ∷ () Source #

d_Bit_10 ∷ () Source #

d_0b_12 ∷ T_Fin_6 Source #

d_1b_14 ∷ T_Fin_6 Source #

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

du_toNatDigits_20 ∷ Integer → Integer → [Integer] Source #

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

du_aux_38 ∷ Integer → Integer → [Integer] → [Integer] Source #

d_q'60'n_74 ∷ Integer → Integer → T_'8868'_6 → Integer → (Integer → T__'8804'__18 → T_Acc_42) → [Integer] → T__'8804'__18 Source #

du_q'60'n_74 ∷ Integer → Integer → T__'8804'__18 Source #

d_Expansion_76 ∷ Integer → () Source #

d_fromDigits_82 ∷ Integer → [T_Fin_6] → Integer Source #

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

du_toDigits_98 ∷ Integer → Integer → T_Σ_14 Source #

d_base_108 ∷ Integer → T_'8868'_6 → Integer → Integer Source #

du_base_108 ∷ Integer → Integer Source #

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

d_cons_120 ∷ Integer → T_'8868'_6 → Integer → Integer → T_Fin_6 → T_Σ_14 → T_Σ_14 Source #

du_cons_120 ∷ T_Fin_6 → T_Σ_14 → T_Σ_14 Source #

d_lem_136 ∷ Integer → T_'8868'_6 → Integer → Integer → Integer → Integer → T__'8804''8242'__154 Source #

du_lem_136 ∷ Integer → Integer → Integer → T__'8804''8242'__154 Source #

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

du_helper_152 ∷ Integer → Integer → (Integer → T__'8804''8242'__154 → T_Σ_14) → T_Σ_14 Source #

d_digitChars_172 ∷ T_Vec_24 Source #

d_showDigit_178 ∷ Integer → AgdaAny → T_Fin_6 → T_Char_6 Source #

du_showDigit_178 ∷ T_Fin_6 → T_Char_6 Source #