← Back to branch summary

~ubuntu-branches/ubuntu/utopic/agda-stdlib/utopic-proposed

« back to all changes in this revision

Viewing changes to src/Data/String.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 09:46:46 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805094646-zqd0c4m8ndngqg6x
Tags: 0.8-1
* [4ca6fd0] Update debian/watch to fetch tarballs from github
* [84d4313] Imported Upstream version 0.8
* [7b08243] debian/control: Require agda 2.4.x per upstream
* [37e7e10] debian/control: Standards-Version → 3.9.5, no changes required.
* [9051b9d] Run upstream's "GenerateEverything" script

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/String.agda
13
13
open import Data.Bool using (Bool; true; false)
14
14
open import Function
15
15
open import Relation.Nullary
 
16
open import Relation.Nullary.Decidable
16
17
open import Relation.Binary
17
18
open import Relation.Binary.List.StrictLex as StrictLex
18
19
import Relation.Binary.On as On
56
57
fromList : List Char → String
57
58
fromList = primStringFromList
58
59
 
 
60
toList∘fromList : ∀ s → toList (fromList s) ≡ s
 
61
toList∘fromList s = trustMe
 
62
 
 
63
fromList∘toList : ∀ s → fromList (toList s) ≡ s
 
64
fromList∘toList s = trustMe
 
65
 
59
66
toVec : (s : String) → Vec Char (List.length (toList s))
60
67
toVec s = Vec.fromList (toList s)
61
68
 
66
73
unlines []       = ""
67
74
unlines (x ∷ xs) = x ++ "\n" ++ unlines xs
68
75
 
69
 
infix 4 _==_
70
 
 
71
 
_==_ : String → String → Bool
72
 
_==_ = primStringEquality
 
76
-- Informative equality test.
73
77
 
74
78
_≟_ : Decidable {A = String} _≡_
75
 
s₁ ≟ s₂ with s₁ == s₂
 
79
s₁ ≟ s₂ with primStringEquality s₁ s₂
76
80
... | true  = yes trustMe
77
81
... | false = no whatever
78
82
  where postulate whatever : _
79
83
 
 
84
-- Boolean equality test.
 
85
--
 
86
-- Why is the definition _==_ = primStringEquality not used? One
 
87
-- reason is that the present definition can sometimes improve type
 
88
-- inference, at least with the version of Agda that is current at the
 
89
-- time of writing: see unit-test below.
 
90
 
 
91
infix 4 _==_
 
92
 
 
93
_==_ : String → String → Bool
 
94
s₁ == s₂ = ⌊ s₁ ≟ s₂ ⌋
 
95
 
 
96
private
 
97
 
 
98
  -- The following unit test does not type-check (at the time of
 
99
  -- writing) if _==_ is replaced by primStringEquality.
 
100
 
 
101
  data P : (String → Bool) → Set where
 
102
    p : (c : String) → P (_==_ c)
 
103
 
 
104
  unit-test : P (_==_ "")
 
105
  unit-test = p _
 
106
 
80
107
setoid : Setoid _ _
81
108
setoid = PropEq.setoid String
82
109