------------------------------------------------------------------------
-- The Agda standard library
--
-- Unsafe String operations and proofs
------------------------------------------------------------------------
{-# OPTIONS --with-K #-}
module Data.String.Unsafe where
import Data.List.Base as List using (List; _∷_; _++_; length; replicate; tail)
import Data.List.Properties as Listₚ using (length-replicate; length-++)
open import Data.Maybe.Base using (maybe′)
open import Data.Nat.Base using (zero; suc; _+_)
open import Data.Product.Base using (proj₂)
open import Data.String.Base
using (String; toList; fromList; length; tail; _++_; replicate)
open import Function.Base using (_∘′_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)
open ≡-Reasoning
------------------------------------------------------------------------
-- Properties of tail
length-tail : ∀ s → length s ≡ maybe′ (suc ∘′ length) zero (tail s)
length-tail s = 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
toList-++ : ∀ s t → toList (s ++ t) ≡ toList s List.++ toList t
toList-++ s t = trustMe
length-++ : ∀ s t → length (s ++ t) ≡ length s + length t
length-++ s t = begin
length (s ++ t) ≡⟨⟩
List.length (toList (s ++ t)) ≡⟨ cong List.length (toList-++ s t) ⟩
List.length (toList s List.++ toList t) ≡⟨ Listₚ.length-++ (toList s) ⟩
length s + length t ∎
length-replicate : ∀ n {c} → length (replicate n c) ≡ n
length-replicate n {c} = let cs = List.replicate n c in begin
length (replicate n c) ≡⟨ cong List.length (toList∘fromList cs) ⟩
List.length cs ≡⟨ Listₚ.length-replicate n ⟩
n ∎
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4