DaveCTurner

theory Leftpad
  imports Main
begin

definition leftPad :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list"
  where "leftPad padChar targetLength s ≡ replicate (targetLength - length s) padChar @ s"

definition isPadded :: "'a ⇒ 'a list ⇒ 'a list ⇒ bool"
  where "isPadded padChar unpadded padded ≡ ∃ n. set (take n padded) ⊆ { padChar } ∧ drop n padded = unpadded"