Skip to content

Instantly share code, notes, and snippets.

@useronym

useronym/takeWhile-repeat.agda

Last active July 26, 2016 15:43
Show Gist options
  • Save useronym/07223deaecebadb87b6d286e699d12c7 to your computer and use it in GitHub Desktop.
Save useronym/07223deaecebadb87b6d286e699d12c7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
takeWhile-repeat.agda
open import Data.List
open import Data.Nat.Base
open import Data.Bool.Base
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
repeat : ∀ {l} {A : Set l} → ℕ → A → List A
repeat zero x = []
repeat (suc n) x = x ∷ repeat n x
takeWhile-repeat : ∀ {l} {A : Set l} {p : A → Bool} {a : A} {n : ℕ} → p a ≡ true → takeWhile p (repeat n a) ≡ repeat n a
takeWhile-repeat {n = 0} pf = refl
takeWhile-repeat {n = suc n'} pf rewrite pf = { }0
-- takeWhile-repeat {n = suc n'} pf rewrite pf | takeWhile-repeat {n = n'} pf = {!!}
@Saizan
Copy link

Saizan commented Jul 26, 2016 

open import Data.List
open import Data.Nat.Base
open import Data.Bool.Base
open import Relation.Binary.PropositionalEquality using (_≡_; refl)


repeat : ∀ {l} {A : Set l} → ℕ → A → List A
repeat zero x = []
repeat (suc n) x = x ∷ repeat n x

takeWhile-repeat : ∀ {l} {A : Set l} {p : A → Bool} {a : A} {n : ℕ} → p a ≡ true → takeWhile p (repeat n a) ≡ repeat n a
takeWhile-repeat {n = 0} pf = refl
takeWhile-repeat {p = p} {n = suc n'} pf rewrite pf | takeWhile-repeat {p = p} {n = n'} pf = refl

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment