← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/Data/Nat/Show.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Nat/Show.agda
10
10
open import Relation.Nullary.Decidable using (True)
11
11
open import Data.String as String using (String)
12
12
open import Data.Digit
 
13
open import Data.Product using (proj₁)
13
14
open import Function
14
15
open import Data.List
15
16
 
24
25
  String.fromList $
25
26
  map (showDigit {base≤16 = base≤16}) $
26
27
  reverse $
27
 
  theDigits base {base≥2 = base≥2} n
 
28
  proj₁ $ toDigits base {base≥2 = base≥2} n
28
29
 
29
30
-- show n is a string containing the decimal expansion of n (starting
30
31
-- with the most significant digit).