잇창명 EatChangmyeong💕🐱 @pub.eatch.dev · 13d 큰일났다 아그다 안쓴지 너무 오래돼서 어떻게 쓰는지 다까먹었네... 이거 어떻게 증명하더라 코드 private variable a : Level A : Set a split : List A → List (List A × List A) split [] = ([] , []) ∷ [] split (x ∷ xs) = ([] , x ∷ xs) ∷ map (λ (fst […] [Original post on hackers.pub]
1 likes 3 replies
?
Replies
내가해냄!!!! 코드 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⁺ […] [Original post on hackers.pub]
VSCode agda-mode에서 제일 짜증나는 점... 역슬래시로 유니코드 입력 모드에 진입하면 가끔씩 입력이 제대로 안된다. 특히 `\==\<\>` → `≡⟨⟩`나 `\^+` = `⁺`에서 심하게 느껴진다
아맞다 여기서는 알트텍스트에 줄바꿈이 안되지