← Back to branch summary

~ubuntu-branches/ubuntu/precise/agda-stdlib/precise

« back to all changes in this revision

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

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (2.1.4 sid)
  • Revision ID: package-import@ubuntu.com-20111129170035-be8cbok8ojft5tjl
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Nat/Show.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Showing natural numbers
3
5
------------------------------------------------------------------------
4
6
 
18
20
             {base≥2 : True (2 ≤? base)}
19
21
             {base≤16 : True (base ≤? 16)} →
20
22
             ℕ → String
21
 
showInBase base {base≥2} {base≤16} =
22
 
  String.fromList ∘
23
 
  map (showDigit {base≤16 = base≤16}) ∘
24
 
  reverse ∘
25
 
  theDigits base {base≥2 = base≥2}
 
23
showInBase base {base≥2} {base≤16} n =
 
24
  String.fromList $
 
25
  map (showDigit {base≤16 = base≤16}) $
 
26
  reverse $
 
27
  theDigits base {base≥2 = base≥2} n
26
28
 
27
29
-- show n is a string containing the decimal expansion of n (starting
28
30
-- with the most significant digit).