StringNat.agda

module StringNat where

open import Agda.Builtin.Char
open import Agda.Builtin.List
open import Data.Unit
open import Data.Bool
open import Data.Product
open import Function

data CharView : Char → Set where
  CharZ : CharView 'z'
  CharS : CharView 's'
  Other : ∀ {c} → CharView c

charView : ∀ c → CharView c
charView 'z' = CharZ
charView 's' = CharS
charView c   = Other

ℕ' : List Char → Bool
ℕ' []       = false
ℕ' (c ∷ cs) with charView c
ℕ' (.'z' ∷ cs) | CharZ = case cs of λ { [] → true ; _ → false }
ℕ' (.'s' ∷ cs) | CharS = ℕ' cs
ℕ' (c ∷ cs)    | Other = false

ℕ : Set
ℕ = ∃ (T ∘ ℕ')

pred : ℕ → ℕ
pred ([] , ())
pred (c ∷ cs , pr) with charView c
pred (.'z' ∷ [] , pr)    | CharZ = 'z' ∷ [] , tt
pred (.'z' ∷ _ ∷ _ , ()) | CharZ
pred (.'s' ∷ cs , pr) | CharS = cs , pr
pred (c ∷ cs , ()) | Other