open import Logic
open import Nat
open import Eq
open import Bool
open import Maybe
open import Decide
open import List
open import Vec
module Talk where
badlyNamed : ∀ {A} → (A → A → Bool) → List A → List A → Bool
badlyNamed _==_ [] ys = true
badlyNamed _==_ (x ∷ xs) [] = false
badlyNamed _==_ (x ∷ xs) (y ∷ ys) = (x == y) && badlyNamed _==_ xs ys
data Prefix {A n} (xs : Vec A n) : ∀ {m} → Vec A m → Set where
prefix : ∀ {m} (zs : Vec A m) → Prefix xs (xs ++ zs)
isPrefixOf : ∀ {A n m} → ((x y : A) → Maybe (x ≡ y)) →
(xs : Vec A n) (ys : Vec A m) → Maybe (Prefix xs ys)
isPrefixOf _==_ [] ys = just (prefix ys)
isPrefixOf _==_ (x ∷ xs) [] = nothing
isPrefixOf _==_ (x ∷ xs) (y ∷ ys) with x == y
isPrefixOf _==_ (x ∷ xs) (y ∷ ys) | nothing = nothing
isPrefixOf _==_ (x ∷ xs) (.x ∷ ys) | just refl with isPrefixOf _==_ xs ys
isPrefixOf _==_ (x ∷ xs) (.x ∷ ys) | just refl | nothing = nothing
isPrefixOf _==_ (x ∷ xs) (.x ∷ .(xs ++ zs)) | just refl | just (prefix zs) =
just (prefix zs)
clickDecToJumpToItsDefinition = Dec
noHd : ∀ {A m n}{x y : A}{xs : Vec A n}{ys : Vec A m} → ¬ x ≡ y → ¬ Prefix (x ∷ xs) (y ∷ ys)
noHd prf (prefix zs) = prf refl
noTl : ∀ {A m n}{x y : A}{xs : Vec A n}{ys : Vec A m} → ¬ Prefix xs ys → ¬ Prefix (x ∷ xs) (y ∷ ys)
noTl prf (prefix zs) = prf (prefix zs)
isPrefixOf′ : ∀ {A n m} → ((x y : A) → Dec (x ≡ y)) →
(xs : Vec A n) (ys : Vec A m) → Dec (Prefix xs ys)
isPrefixOf′ _==_ [] ys = yes (prefix ys)
isPrefixOf′ _==_ (x ∷ xs) [] = no λ ()
isPrefixOf′ _==_ (x ∷ xs) (y ∷ ys) with x == y
isPrefixOf′ _==_ (x ∷ xs) (y ∷ ys) | no np = no (noHd np)
isPrefixOf′ _==_ (x ∷ xs) (.x ∷ ys) | yes refl with isPrefixOf′ _==_ xs ys
isPrefixOf′ _==_ (x ∷ xs) (.x ∷ ys) | yes refl | no np = no (noTl np)
isPrefixOf′ _==_ (x ∷ xs) (.x ∷ .(xs ++ zs)) | yes refl | yes (prefix zs) = yes (prefix zs)