잇창명 EatChangmyeong💕🐱
@pub.eatch.dev
9 followers 1 following 201 posts
*Encounter the Wider World* 🌉 bridged from ⁂ hackers.pub/@eatch, follow @ap.brid.gy to interact
*Encounter the Wider World* 🌉 bridged from ⁂ hackers.pub/@eatch, follow @ap.brid.gy to interact
![data Foo : Set where
foo : List Foo → Foo
foo-flatten-good : Foo → List Foo
foo-flatten-good (foo []) = []
foo-flatten-good (foo (x ∷ xs)) with foo-flatten-good x | foo-flatten-good (foo xs)
... | x' | xs' = x' ++ xs'
foo-flatten-bad : Foo → List Foo
foo-flatten-bad (foo []) = []
foo-flatten-bad (foo (x ∷ xs)) with foo-flatten-bad x
... | x' with foo-flatten-bad (foo xs)
... | xs' = x' ++ xs'](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:aw4qpzo3cst5ucqxh5ute3y7/bafkreibfyojsxvzbk2gkhc52y4fkhrf2wg6zsqgpjpmh7zmespnvbbkdtq)
![splits-length :
(n : ℕ) →
(xs : List A) →
All (λ ss → length ss ≡ n) (splits n xs)
splits-length zero [] = refl ∷ []
splits-length zero (x ∷ xs) = []
splits-length (suc n) xs =
concat⁺
(gmap⁺
(λ refl -> gmap⁺ (cong suc) (splits-length n _))
(split-correct xs)
)](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:aw4qpzo3cst5ucqxh5ute3y7/bafkreidum42gsklwnrqgthctpczvqffrkhfkt4tvi42t7ajhcvijdhciey)
![private
variable
a : Level
A : Set a
split : List A → List (List A × List A)
split [] = ([] , []) ∷ []
split (x ∷ xs) =
([] , x ∷ xs) ∷
map
(λ (fst , snd) → x ∷ fst , snd)
(split xs)
splits : ℕ → List A → List (List (List A))
splits zero [] = [] ∷ []
splits zero (x ∷ xs) = []
splits (suc n) xs =
concatMap
(λ (fst , snd) → map (fst ∷_) (splits n snd))
(split xs)
splits-length :
(n : ℕ) →
(xs : List A) →
All (λ ss → length ss ≡ n) (splits n xs)
splits-length zero [] = refl ∷ []
splits-length zero (x ∷ xs) = []
splits-length (suc n) [] with splits n [] | splits-length n []
... | ss | pxs = ?
splits-length (suc n) (x ∷ xs) = ?
*All Goals*
?0 : All (λ ss₁ → Data.List.foldr (λ _ → suc) 0 ss₁ ≡ suc n) (map (_∷_ []) (splits n []) ++ [])
?1 : All (λ ss → length ss ≡ suc n) (splits (suc n) (x ∷ xs))
_A.a_273 : Level
_A_274 : Set _A.a_273
_A.a_275 : Level
_A_276 : Set _A.a_275](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:aw4qpzo3cst5ucqxh5ute3y7/bafkreibi5ujepzhyi3al2lkzmz5xuxwxnyr4y6erkmkew2uvrfkyilue3m)
![Agda의 오류 메시지:
[검열됨]/regex.agda:148,1-12: error: [ShouldBeEmpty]
¬ ch ≡ ch should be empty, but that's not obvious to me
when checking the clause left hand side
Regex.with-328 N = N ch (no ())](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:aw4qpzo3cst5ucqxh5ute3y7/bafkreigur55f6q3jgbydvzctacu5icllp3y6w4pyaxh44vzaytwlp4raiy)
