*Encounter the Wider World* 🌉 bridged from ⁂ https://hackers.pub/@eatch, follow @ap.brid.gy to interact
![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)
![Claude 웹 인터페이스에서 parent_message_uuid: Input should be a valid UUID, invalid character: expected an optional prefix of `urn:uuid:` followed by [0-9a-fA-F-], found `n` at 1 오류가 발생했다.](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:aw4qpzo3cst5ucqxh5ute3y7/bafkreibpgjs3ybvljryqxau7gstbandrcyjzrhgerywwbuz4mbyshq57ei)
*Encounter the Wider World* 🌉 bridged from ⁂ https://hackers.pub/@eatch, follow @ap.brid.gy to interact