------------------------------------------------------------------------ -- The Agda standard library -- -- Unsafe String operations and proofs ------------------------------------------------------------------------ {-# OPTIONS --with-K #-} module Data.String.Unsafe where open import Data.String.Base open import Relation.Binary.PropositionalEquality using (_≡_) open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe) ------------------------------------------------------------------------ -- Properties of conversion functions toList∘fromList : ∀ s → toList (fromList s) ≡ s toList∘fromList s = trustMe fromList∘toList : ∀ s → fromList (toList s) ≡ s fromList∘toList s = trustMe